harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
theorem equiv_of_iso (o : HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι}
    {g : β → ι} (i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) :
    ∃ e : α ≃ β, ∀ a, g (e a) = f a

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.inv c * o.matrixDecomposition i.hom c = 1

Tactic:
rw [← o.matrixDecomposition_comp]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition (i.hom ≫ i.inv) c = 1

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition (i.inv ≫ i.hom) c = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ (c : ι) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})

Tactic:
intro c

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Nonempty (↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))

Tactic:
apply Cardinal.eq.1

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem LinearIndependent.map_of_isPurelyInseparable_of_isSeparable [IsPurelyInseparable F E]
    {ι : Type*} {v : ι → K} (hsep : ∀ i : ι, IsSeparable F (v i))
    (h : LinearIndependent F v) : LinearIndependent E v

Proof state:
case intro
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
⊢ l i = 0 i

Tactic:
let n := l.support.sup f

Result:
case intro
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
⊢ l i = 0 i
-- Mathlib/Topology/Gluing.lean
theorem fromOpenSubsetsGlue_isOpenMap : IsOpenMap (fromOpenSubsetsGlue U)

Proof state:
case right.right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
    ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s ∩ Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Tactic:
refine ⟨Set.mem_image_of_mem _ hx, ?_⟩

Result:
case right.right
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
i : (ofOpenSubsets U).J
x : ↑(of α)
hx' : x ∈ U i
hx : (ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩ ∈ s
⊢ (ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⟨x, hx'⟩) ∈
    Set.range ⇑(ConcreteCategory.hom (U i).inclusion')

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
rw [isOpen_iff_forall_mem_open]

Result:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ ∀ x ∈ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s, IsOpen t ∧ x ∈ t

Proof state:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : IsOpen s
⊢ IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
rw [(ofOpenSubsets U).isOpen_iff] at hs

Result:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)
-- Mathlib/Algebra/Homology/Embedding/Restriction.lean
@[reassoc]
lemma restrictionMap_f' {i : ι} {i' : ι'} (hi : e.f i = i') :
    (restrictionMap φ e).f i = (K.restrictionXIso e hi).hom ≫
      φ.f i' ≫ (L.restrictionXIso e hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
⊢ (restrictionMap φ e).f i = (K.restrictionXIso e hi).hom ≫ φ.f i' ≫ (L.restrictionXIso e hi).inv

Tactic:
subst hi

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (restrictionMap φ e).f i = (K.restrictionXIso e ⋯).hom ≫ φ.f (e.f i) ≫ (L.restrictionXIso e ⋯).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (restrictionMap φ e).f i = (K.restrictionXIso e ⋯).hom ≫ φ.f (e.f i) ≫ (L.restrictionXIso e ⋯).inv

Tactic:
simp [restrictionXIso]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
lemma IsCoprime.intCast {R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :
    IsCoprime (a : R) (b : R)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : ℤ
h : IsCoprime a b
⊢ IsCoprime ↑a ↑b

Tactic:
rcases h with ⟨u, v, H⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ IsCoprime ↑a ↑b

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑1 = 1

Tactic:
exact Int.cast_one

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑u * ↑a + ↑v * ↑b = 1

Tactic:
rw_mod_cast [H]

Result:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑1 = 1

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ IsCoprime ↑a ↑b

Tactic:
use u, v

Result:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑u * ↑a + ↑v * ↑b = 1
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_three : normEDS b c d 3 = c

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 3 = c

Tactic:
erw [normEDS_ofNat, preNormEDS'_three, if_neg <| by decide, mul_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ ¬Even 3

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_coe_unitary_mul (U : unitary E) (A : E) : ‖(U : E) * A‖ = ‖A‖

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖(↑U)⋆ * ↑U * A‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖

Tactic:
rw [mul_assoc]

Result:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖

Proof state:
case refine_1
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖

Tactic:
calc
  _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
  _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]

Result:
no goals

Proof state:
case refine_2
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖

Tactic:
calc
  _ = ‖(U : E)⋆ * U * A‖ := by rw [unitary.coe_star_mul_self U, one_mul]
  _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
    rw [mul_assoc]
    exact norm_mul_le _ _
  _ = ‖(U : E) * A‖ := by rw [norm_star, norm_coe_unitary, one_mul]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖↑U‖ * ‖A‖ = ‖A‖

Tactic:
rw [norm_coe_unitary, one_mul]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖(↑U)⋆ * (↑U * A)‖ ≤ ‖(↑U)⋆‖ * ‖↑U * A‖

Tactic:
exact norm_mul_le _ _

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖(↑U)⋆‖ * ‖↑U * A‖ = ‖↑U * A‖

Tactic:
rw [norm_star, norm_coe_unitary, one_mul]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖A‖ = ‖(↑U)⋆ * ↑U * A‖

Tactic:
rw [unitary.coe_star_mul_self U, one_mul]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
nontriviality E

Result:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖↑U * A‖ ≤ ‖A‖

case refine_2
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
a✝ : Nontrivial E
⊢ ‖A‖ ≤ ‖↑U * A‖
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_span_iff_mem_addSubgroup_closure_nonunital {s : Set R} {z : R} :
    z ∈ span s ↔ z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Proof state:
case refine_1
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
rintro x y (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
  ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)

Result:
case refine_1.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
⊢ x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_1.inl.inl.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 => x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_1.inl.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 => x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 => x1 * x2) ((fun x1 x2 => x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Proof state:
case refine_1.inl.inr.intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 => x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inr <| ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem Balanced.sub (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s - t)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_eq_veblenWith_iff :
    veblenWith f o₁ a = veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a = veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
rw [← cmp_eq_eq_iff, cmp_veblenWith hf]

Result:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.eq ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.eq ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
aesop (add simp lt_asymm)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma add_le_mul {a : ℕ} (ha : 2 ≤ a) : ∀ {b : ℕ} (_ : 2 ≤ b), a + b ≤ a * b
  | 2, _ => by omega
  | b + 3, _ => by have := Nat.add_le_mul ha (Nat.le_add_left _ b); rw [mul_succ]; omega

Proof state:
a : ℕ
ha : 2 ≤ a
b : ℕ
x✝ : 2 ≤ b + 3
this : a + (b + 2) ≤ a * (b + 2)
⊢ a + (b + 3) ≤ a * (b + 3)

Tactic:
rw [mul_succ]

Result:
a : ℕ
ha : 2 ≤ a
b : ℕ
x✝ : 2 ≤ b + 3
this : a + (b + 2) ≤ a * (b + 2)
⊢ a + (b + 3) ≤ a * (b + 2) + a

Proof state:
a : ℕ
ha : 2 ≤ a
b : ℕ
x✝ : 2 ≤ b + 3
this : a + (b + 2) ≤ a * (b + 2)
⊢ a + (b + 3) ≤ a * (b + 2) + a

Tactic:
omega

Result:
no goals

Proof state:
a : ℕ
ha : 2 ≤ a
b : ℕ
x✝ : 2 ≤ b + 3
⊢ a + (b + 3) ≤ a * (b + 3)

Tactic:
have := Nat.add_le_mul ha (Nat.le_add_left _ b)

Result:
a : ℕ
ha : 2 ≤ a
b : ℕ
x✝ : 2 ≤ b + 3
this : a + (b + 2) ≤ a * (b + 2)
⊢ a + (b + 3) ≤ a * (b + 3)

Proof state:
a : ℕ
ha : 2 ≤ a
x✝ : 2 ≤ 2
⊢ a + 2 ≤ a * 2

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i])

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Proof state:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
simp_all [all_eq_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
simp only [all_eq_false] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ i x, ¬p xs[i] = true
⊢ false = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
by_cases h : xs.all p

Result:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ i x, ¬p xs[i] = true
⊢ false = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma singularPart_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
    μ.singularPart ν = 0 ↔ μ ≪ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Tactic:
refine ⟨fun h ↦ ?_, singularPart_eq_zero_of_ac⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν

Tactic:
rw [h_dec]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν

Tactic:
rw [h, zero_add] at h_dec

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous ν _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_eq_getElem?_toList_append {l : List α} {n : Nat} :
    l.drop n = l[n]?.toList ++ l.drop (n + 1)

Proof state:
case cons.succ
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
n✝ : Nat
⊢ drop (n✝ + 1) (hd :: tl) = (hd :: tl)[n✝ + 1]?.toList ++ drop (n✝ + 1 + 1) (hd :: tl)

Tactic:
simp only [drop_succ_cons, getElem?_cons_succ]

Result:
case cons.succ
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
n✝ : Nat
⊢ drop n✝ tl = tl[n✝]?.toList ++ drop (n✝ + 1) tl

Proof state:
case nil
α : Type u_1
n : Nat
⊢ drop n [] = [][n]?.toList ++ drop (n + 1) []

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
n✝ : Nat
⊢ drop n✝ tl = tl[n✝]?.toList ++ drop (n✝ + 1) tl

Tactic:
rw [ih]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
⊢ drop 0 (hd :: tl) = (hd :: tl)[0]?.toList ++ drop (0 + 1) (hd :: tl)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
n : Nat
⊢ drop n (hd :: tl) = (hd :: tl)[n]?.toList ++ drop (n + 1) (hd :: tl)

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
⊢ drop 0 (hd :: tl) = (hd :: tl)[0]?.toList ++ drop (0 + 1) (hd :: tl)

case cons.succ
α : Type u_1
hd : α
tl : List α
ih : ∀ {n : Nat}, drop n tl = tl[n]?.toList ++ drop (n + 1) tl
n✝ : Nat
⊢ drop (n✝ + 1) (hd :: tl) = (hd :: tl)[n✝ + 1]?.toList ++ drop (n✝ + 1 + 1) (hd :: tl)