internlm/Lean-Github huggingface dataset:
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have qAB := online_3_of_B Hq.1 bAB aAB
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have pAB := online_3_of_B Hp.1 qAB aAB
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have := (on_circle_iff_length_eq hC.1 Hp.2).mpr hC.2
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
rw [← this] at Hq
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
rw [Hq.2] at big
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have bp : b ≠ p := fun bp => by
  rw [←bp, bp] at Hq; rw [bp] at big
  simp [lt_self_iff_false] at big
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
have ap := (ne_12_of_B (B_symm Hp.1)).symm
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ ∃ p, B a b p ∧ length a p = length c d
Tactic:
refine' ⟨p, _, Hq.2.symm⟩
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ B a b p
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
⊢ B a b p
Tactic:
have B3 := B_of_three_online_ne_short big ab ap bp aAB bAB pAB
Proof state after:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p ∨ B b a p
⊢ B a b p
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p ∨ B b a p
⊢ B a b p
Tactic:
cases B3 with
| inl B3 => exact B3
| inr B3 => exfalso; exact (not_B324_of_B123_B124 (B_symm Hq.1) Hp.1) B3
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c = d
⊢ False
Tactic:
rw [cd, length_eq_zero_iff.mpr rfl] at big
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c = d
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c = d
⊢ False
Tactic:
exact not_lt_of_ge (length_nonneg a b) big
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b a q ∧ length c d = length a q
aq : a = q
⊢ False
Tactic:
rw [aq, length_eq_zero_iff.mpr rfl] at Hq
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < length c d
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Tactic:
rw [Hq.2] at big
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
big : length a b < 0
cd : c ≠ d
q : point
Hq : B b q q ∧ length c d = 0
aq : a = q
⊢ False
Tactic:
exact not_lt_of_ge (length_nonneg a b) big
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
rw [←bp, bp] at Hq
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
rw [bp] at big
Proof state after:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a p < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a p < length a p
Hq : B p a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b = p
⊢ False
Tactic:
simp [lt_self_iff_false] at big
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro.inl
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B a b p
⊢ B a b p
Tactic:
exact B3
Proof state after:
no goals
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro.inr
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ B a b p
Tactic:
exfalso
Proof state after:
case intro.intro.intro.intro.intro.inr.h
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ False
Theorem: same_length_B_of_ne_ge
Proof state before:
case intro.intro.intro.intro.intro.inr.h
i : incidence_geometry
a b c d : point
ab : a ≠ b
cd : c ≠ d
q : point
aq : a ≠ q
C : circle
hC : center_circle a C ∧ on_circle q C
p : point
big : length a b < length a p
Hq : B b a q ∧ length c d = length a p
Hp : B q a p ∧ on_circle p C
AB : line
aAB : online a AB
bAB : online b AB
qAB : online q AB
pAB : online p AB
this : length a p = length a q
bp : b ≠ p
ap : a ≠ p
B3 : B b a p
⊢ False
Tactic:
exact (not_B324_of_B123_B124 (B_symm Hq.1) Hp.1) B3
Proof state after:
no goals
Theorem: para_len_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
⊢ para N O
Tactic:
have abc_bcd := alternate_eq_of_para aL bL bP cP cM dM aPd pLM
Proof state after:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ para N O
Theorem: para_len_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ para N O
Tactic:
obtain ⟨-, -, bca_cbd⟩ := sas (by perma) (by perm) (by perma)
Proof state after:
case intro.intro
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
bca_cbd : angle ?m.55016 ?m.55020 ?m.55017 = angle ?m.55018 ?m.55021 ?m.55019
⊢ para N O
Theorem: para_len_parallelogram
Proof state before:
case intro.intro
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
bca_cbd : angle ?m.55016 ?m.55020 ?m.55017 = angle ?m.55018 ?m.55021 ?m.55019
⊢ para N O
Tactic:
exact para_of_ang_eq cb aN cN cP bP bO dO aPd bca_cbd
Proof state after:
no goals
Theorem: para_len_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ length b a = length c d
Tactic:
perma
Proof state after:
no goals
Theorem: para_len_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ length b c = length c b
Tactic:
perm
Proof state after:
no goals
Theorem: para_len_parallelogram
Proof state before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ angle a b c = angle d c b
Tactic:
perma
Proof state after:
no goals
Theorem: eq_of_parallelogram_of_eq_basis_of_diffside
Proof state before:
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
obtain ⟨ Q, bQ, eQ ⟩ := line_of_pts b e
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis_of_diffside
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
obtain ⟨ R, cR, hR ⟩ := line_of_pts c h
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis_of_diffside
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have ec : e ≠ c := neq_of_para eL cM pLM
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Theorem: eq_of_parallelogram_of_eq_basis_of_diffside
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
⊢ area a b c + area a d c = area e f g + area e h g
Tactic:
have ehgf : paragram e h g f L P M O := by splitAll <;> perma only [para]
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f g h : point
L M K N O P : line
aL : online a L
dL : online d L
eL : online e L
hL : online h L
bM : online b M
cM : online c M
fM : online f M
gM : online g M
aK : online a K
bK : online b K
dN : online d N
cN : online c N
eO : online e O
fO : online f O
hP : online h P
gP : online g P
pLM : para L M
pKN : para K N
pOP : para O P
hlen : length b c = length f g
S : line
cS : online c S
eS : online e S
aPd : diffside b h S
bc : b ≠ c
Q : line
bQ : online b Q
eQ : online e Q
R : line
cR : online c R
hR : online h R
ec : e ≠ c
ehgf : paragram e h g f L P M O
⊢ area a b c + area a d c = area e f g + area e h g