def EuclidGeom.liftOrElse {m : Type u_1 → Type u_2} {A : Type u_1} [Monad m] (xs : m (Option A)) (ys : m (Option A)) : m (Option A)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.extractSegLengthEq (expr : Q(Prop)) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.extractAngleValueEq (expr : Q(Prop)) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.getCongrDeclNames : Lean.Elab.Tactic.TacticM (List Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.congrSaLemmas : List Lean.Name

Equations

• EuclidGeom.congrSaLemmas = [`EuclidGeom.TriangleND.congr_of_SAS, `EuclidGeom.TriangleND.congr_of_ASA, `EuclidGeom.TriangleND.congr_of_AAS]

def EuclidGeom.congr_sa : Lean.ParserDescr

Equations

• EuclidGeom.congr_sa = Lean.ParserDescr.node `EuclidGeom.congr_sa 1024 (Lean.ParserDescr.nonReservedSymbol "congr_sa" false)

def EuclidGeom.evalCongrSa : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.CONGR_SA : Lean.ParserDescr

Equations

• EuclidGeom.CONGR_SA = Lean.ParserDescr.node `EuclidGeom.CONGR_SA 1024 (Lean.ParserDescr.nonReservedSymbol "CONGR_SA" false)

def EuclidGeom.evalCONGRSA : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.extractNegAngleValueEq (expr : Q(Prop)) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.getACongrDeclNames : Lean.Elab.Tactic.TacticM (List Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.acongrSaLemmas : List Lean.Name

Equations

• EuclidGeom.acongrSaLemmas = [`EuclidGeom.TriangleND.acongr_of_SAS, `EuclidGeom.TriangleND.acongr_of_ASA, `EuclidGeom.TriangleND.acongr_of_AAS]

def EuclidGeom.acongr_sa : Lean.ParserDescr

Equations

• EuclidGeom.acongr_sa = Lean.ParserDescr.node `EuclidGeom.acongr_sa 1024 (Lean.ParserDescr.nonReservedSymbol "acongr_sa" false)

def EuclidGeom.evalACongrSa : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.ACONGR_SA : Lean.ParserDescr

Equations

• EuclidGeom.ACONGR_SA = Lean.ParserDescr.node `EuclidGeom.ACONGR_SA 1024 (Lean.ParserDescr.nonReservedSymbol "ACONGR_SA" false)

def EuclidGeom.evalACONGRSA : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.