internlm/Lean-Github huggingface dataset:
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
leq : length d e = length a b
⊢ ¬colinear a c b
Tactic:
perma
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
leq : length d e = length a b
⊢ ¬colinear d f e
Tactic:
perma
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
leq : length d e = length a b
⊢ angle c a b = angle f d e
Tactic:
perma
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
leq : length d e = length a b
⊢ angle a b c = angle d e f
Tactic:
perma [abc_def]
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
⊢ triangle a c b
Tactic:
perma
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ False
Tactic:
rw [hg] at Hh
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ False
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ False
Tactic:
have := online_3_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ False
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ False
Tactic:
exact (online_3_of_triangle aAC cAC (by perma)) this
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ triangle a c b
Tactic:
perma
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ angle h a g = angle b a c
Tactic:
linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_12_of_B Hh.1) Hg.1]
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
hag_bac : angle h a g = angle b a c
⊢ angle g a h = angle f d e
Tactic:
linperm
Proof state after:
no goals
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g AB
⊢ False
Tactic:
rw [line_unique_of_pts (ne_12_of_B Hg.1) aAB gAB aAC gAC] at bAB
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AC
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g AB
⊢ False
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
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AC
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g AB
⊢ False
Tactic:
exact bAC bAB
Proof state after:
no goals
Theorem: MulEquiv.mem_iff_map_mem_units_of_mem_iff_map_mem
Proof state before:
G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : Monoid M
e : G ≃* Mˣ
S : Subgroup G
T : Submonoid M
h : ∀ (s : G), s ∈ S ↔ ↑(e s) ∈ T
s : G
⊢ s ∈ S ↔ e s ∈ T.units
Tactic:
simp_rw [Submonoid.mem_units_iff, ← e.map_inv, ← h, iff_self_and, inv_mem_iff, imp_self]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_apply
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ piFinSuccCastSucc v = ((v 0, v (last (n + 1))), v ∘ fun i => i.castSucc.succ)
Tactic:
simp_rw [Prod.ext_iff, Function.funext_iff]
Proof state after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ ((piFinSuccCastSucc v).1.1 = v 0 ∧ (piFinSuccCastSucc v).1.2 = v (last (n + 1))) ∧
    ∀ (a : Fin n), (piFinSuccCastSucc v).2 a = (v ∘ fun i => i.castSucc.succ) a
Theorem: piFinSuccCastSucc_apply
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ ((piFinSuccCastSucc v).1.1 = v 0 ∧ (piFinSuccCastSucc v).1.2 = v (last (n + 1))) ∧
    ∀ (a : Fin n), (piFinSuccCastSucc v).2 a = (v ∘ fun i => i.castSucc.succ) a
Tactic:
refine' ⟨⟨rfl, rfl⟩, fun _ => _⟩
Proof state after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ (piFinSuccCastSucc v).2 x✝ = (v ∘ fun i => i.castSucc.succ) x✝
Theorem: piFinSuccCastSucc_apply
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ (piFinSuccCastSucc v).2 x✝ = (v ∘ fun i => i.castSucc.succ) x✝
Tactic:
simp_rw [piFinSuccCastSucc, Equiv.instTrans_trans, Equiv.trans_apply, Equiv.prodCongr_apply,
Equiv.piFinSuccAbove_apply, extractNth, succAbove_last]
Proof state after:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ ((Equiv.prodAssoc α α (Fin n → α)).symm
          (Prod.map (⇑(Equiv.refl α)) (fun f => (f (last n), fun j => f j.castSucc)) ((Equiv.piFinSucc (n + 1) α) v))).2
      x✝ =
    (v ∘ fun i => i.castSucc.succ) x✝
Theorem: piFinSuccCastSucc_apply
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
x✝ : Fin n
⊢ ((Equiv.prodAssoc α α (Fin n → α)).symm
          (Prod.map (⇑(Equiv.refl α)) (fun f => (f (last n), fun j => f j.castSucc)) ((Equiv.piFinSucc (n + 1) α) v))).2
      x✝ =
    (v ∘ fun i => i.castSucc.succ) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: piFinSuccCastSucc_apply_fst_fst
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ (piFinSuccCastSucc v).1.1 = v 0
Tactic:
simp_rw [piFinSuccCastSucc_apply]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_apply_fst_snd
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ (piFinSuccCastSucc v).1.2 = v (last (n + 1))
Tactic:
simp_rw [piFinSuccCastSucc_apply]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_apply_snd
Proof state before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ (piFinSuccCastSucc v).2 = v ∘ fun i => i.castSucc.succ
Tactic:
simp only [piFinSuccCastSucc_apply]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_symm_apply_castSucc_succ
Proof state before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
i : Fin n
⊢ piFinSuccCastSucc.symm ((a, b), v) i.castSucc.succ = v i
Tactic:
simp only [piFinSuccCastSucc, Equiv.instTrans_trans, Equiv.symm_trans_apply, Equiv.symm_symm,
  Equiv.prodAssoc_apply, Equiv.prodCongr_symm, Equiv.refl_symm, Equiv.prodCongr_apply,
  Equiv.coe_refl, Equiv.piFinSuccAbove_symm_apply, insertNth_last', Prod_map, id_eq,
  Equiv.piFinSucc_symm_apply, cons_succ, snoc_castSucc]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_symm_apply_succ_castSucc
Proof state before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
i : Fin n
⊢ piFinSuccCastSucc.symm ((a, b), v) i.succ.castSucc = v i
Tactic:
rw [<- succ_castSucc, piFinSuccCastSucc_symm_apply_castSucc_succ]
Proof state after:
no goals
Theorem: piFinSuccCastSucc_symm_apply_last
Proof state before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
⊢ piFinSuccCastSucc.symm ((a, b), v) (last (n + 1)) = b
Tactic:
simp_rw [piFinSuccCastSucc, Equiv.instTrans_trans, Equiv.symm_trans_apply, Equiv.symm_symm,
  Equiv.prodAssoc_apply, Equiv.prodCongr_symm, Equiv.refl_symm, Equiv.prodCongr_apply,
  Equiv.coe_refl, Equiv.piFinSuccAbove_symm_apply, insertNth_last', Prod_map, id_eq,
  Equiv.piFinSucc_symm_apply, cons_snoc_eq_snoc_cons, snoc_last]
Proof state after:
no goals
Theorem: Nat.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ bm = false ∧ bn = true ∧ m = n
Tactic:
refine Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt ?_ ?_
Proof state after:
case refine_1
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bm then Order.succ else id) m < (bif bn then Order.succ else id) n

case refine_2
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bn then id else Order.succ) n < (bif bm then id else Order.succ) m
Theorem: Nat.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case refine_1
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bm then Order.succ else id) m < (bif bn then Order.succ else id) n
Tactic:
cases bm <;> cases bn <;>
simp only [succ_eq_succ, cond_true, cond_false, id_eq] at hnm hmn ⊢ <;> exact hmn
Proof state after:
no goals
Theorem: Nat.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case refine_2
m : ℕ
bm : Bool
n : ℕ
bn : Bool
hmn : (m + bif bm then 1 else 0) < n + bif bn then 1 else 0
hnm : (n + bif bn then 0 else 1) < m + bif bm then 0 else 1
⊢ (bif bn then id else Order.succ) n < (bif bm then id else Order.succ) m
Tactic:
cases bm <;> cases bn <;>
simp only [succ_eq_succ, cond_true, cond_false, id_eq] at hnm hmn ⊢ <;> exact hnm
Proof state after:
no goals
Theorem: Fin.rev_eq_zero_iff_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ i.rev = 0 ↔ i = last m
Tactic:
convert rev_inj
Proof state after:
case h.e'_1.h.e'_3.h
m : ℕ
i : Fin (m + 1)
⊢ 0 = (last m).rev
Theorem: Fin.rev_eq_zero_iff_last
Proof state before:
case h.e'_1.h.e'_3.h
m : ℕ
i : Fin (m + 1)
⊢ 0 = (last m).rev
Tactic:
exact (rev_last m).symm
Proof state after:
no goals
Theorem: Fin.rev_ne_zero_iff_ne_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ i.rev ≠ 0 ↔ i ≠ last m
Tactic:
simp_rw [ne_eq, rev_eq_zero_iff_last]
Proof state after:
no goals
Theorem: Fin.rev_pos_iff_lt_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ 0 < i.rev ↔ i < last m
Tactic:
simp_rw [lt_last_iff_ne_last, pos_iff_ne_zero]
Proof state after:
m : ℕ
i : Fin (m + 1)
⊢ i.rev ≠ 0 ↔ i ≠ last m
Theorem: Fin.rev_pos_iff_lt_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ i.rev ≠ 0 ↔ i ≠ last m
Tactic:
exact rev_ne_zero_iff_ne_last
Proof state after:
no goals
Theorem: Fin.eq_zero_iff_rev_eq_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ i = 0 ↔ i.rev = last m
Tactic:
convert rev_rev i ▸ rev_eq_zero_iff_last
Proof state after:
no goals
Theorem: Fin.ne_zero_iff_rev_ne_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ i ≠ 0 ↔ i.rev ≠ last m
Tactic:
convert rev_rev i ▸ rev_ne_zero_iff_ne_last
Proof state after:
no goals
Theorem: Fin.pos_iff_rev_lt_last
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ 0 < i ↔ i.rev < last m
Tactic:
convert rev_rev i ▸ rev_pos_iff_lt_last
Proof state after:
no goals
Theorem: Fin.rev_castSucc_succ
Proof state before:
m : ℕ
i : Fin m
⊢ i.castSucc.succ.rev = i.rev.castSucc.succ
Tactic:
simp_rw [rev_succ, rev_castSucc, succ_castSucc]
Proof state after:
no goals
Theorem: Fin.rev_succ_castSucc
Proof state before:
m : ℕ
i : Fin m
⊢ i.succ.castSucc.rev = i.rev.succ.castSucc
Tactic:
simp_rw [← succ_castSucc, rev_castSucc_succ]
Proof state after:
no goals
Theorem: Fin.castSucc_rev_castSucc
Proof state before:
m : ℕ
i : Fin m
⊢ i.castSucc.rev.castSucc = i.succ.rev.succ
Tactic:
simp_rw [rev_succ, rev_castSucc, succ_castSucc]
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rcases lt_or_le (castSucc i) j with (h | h)
Proof state after:
case inl
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ (j.succAbove i).succAbove (i.predAbove j) = j

case inr
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inl
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rw [succAbove_of_castSucc_lt _ _ h, predAbove_of_castSucc_lt _ _ h,
succAbove_castSucc_of_le, succ_pred]
Proof state after:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i ≤ j.pred ⋯
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i ≤ j.pred ⋯
Tactic:
rw [le_pred_iff, ← castSucc_lt_iff_succ_le]
Proof state after:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i.castSucc < j
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inl.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : i.castSucc < j
⊢ i.castSucc < j
Tactic:
exact h
Proof state after:
no goals
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inr
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ (j.succAbove i).succAbove (i.predAbove j) = j
Tactic:
rw [succAbove_of_le_castSucc _ _ h, predAbove_of_le_castSucc _ _ h,
succAbove_succ_of_le, castSucc_castPred]
Proof state after:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j.castPred ⋯ ≤ i
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j.castPred ⋯ ≤ i
Tactic:
rw [castPred_le_iff]
Proof state after:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j ≤ i.castSucc
Theorem: Fin.succAbove_succAbove_predAbove
Proof state before:
case inr.h
m : ℕ
i : Fin (m + 1)
j : Fin (m + 2)
h : j ≤ i.castSucc
⊢ j ≤ i.castSucc
Tactic:
exact h
Proof state after:
no goals
Theorem: Fin.castSucc_le_succAbove
Proof state before:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc ≤ p.succAbove i
Tactic:
obtain h | h := succAbove_eq_castSucc_or_succ p i <;> rw [h]
Proof state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.succ
⊢ i.castSucc ≤ i.succ
Theorem: Fin.castSucc_le_succAbove
Proof state before:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.succ
⊢ i.castSucc ≤ i.succ
Tactic:
exact (castSucc_lt_succ _).le
Proof state after:
no goals
Theorem: Fin.succAbove_le_succ
Proof state before:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≤ i.succ
Tactic:
obtain h | h := succAbove_eq_castSucc_or_succ p i <;> rw [h]
Proof state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.succAbove i = i.castSucc
⊢ i.castSucc ≤ i.succ