internlm/Lean-Github huggingface dataset:
Theorem: similar_of_AA
Proof state before:
case pos
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
wlog df_ac : length d f = length a c
Proof state after:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
swap
Proof state after:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have := length_eq_of_length_eq Tabc Tdef bac_edf abc_def df_ac
Proof state after:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
rw [this, ← df_ac]
Proof state after:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length a b) (length d f) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length a b) (length d f) (length d f)

case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
exact proportion_eq (length_nonneg a b) (length_nonneg d f) (length_eq_zero_iff.not.mpr ab) (length_eq_zero_iff.not.mpr df)
Proof state after:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
rw [proportion_symm_iff]
Proof state after:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Theorem: similar_of_AA
Proof state before:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Tactic:
have leq : length d e = length a b := by
  cases hlen with
  | inl hlen => exfalso; exact df_ac hlen
  | inr hlen => exact hlen
Proof state after:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Theorem: similar_of_AA
Proof state before:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Tactic:
refine' this (by perma) (by perma) (by perma) _ de ab df ac bc.symm ef.symm (Or.symm hlen) leq
Proof state after:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle a c b = angle d f e
Theorem: similar_of_AA
Proof state before:
case pos.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle a c b = angle d f e
Tactic:
exact (asa Tabc leq.symm bac_edf (by perma [abc_def])).2.2
Proof state after:
no goals
Theorem: similar_of_AA
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
⊢ length d e = length a b
Tactic:
cases hlen with
| inl hlen => exfalso; exact df_ac hlen
| inr hlen => exact hlen
Proof state after:
no goals
Theorem: similar_of_AA
Proof state before:
case inl
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ length d e = length a b
Tactic:
exfalso
Proof state after:
case inl.h
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ False
Theorem: similar_of_AA
Proof state before:
case inl.h
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ False
Tactic:
exact df_ac hlen
Proof state after:
no goals
Theorem: similar_of_AA
Proof state before:
case inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f = length a c ∨ length d e = length a b →
                          length d f = length a c → proportion (length a b) (length d e) (length a c) (length d f)
df_ac : ¬length d f = length a c
hlen : length d e = length a b
⊢ length d e = length a b
Tactic:
exact hlen
Proof state after:
no goals