harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem apply_mem_spectrum [Nontrivial R] (φ : F) (a : A) : φ a ∈ σ a

Proof state:
F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑ₐ (φ a) - a ∈ RingHom.ker ↑φ

Tactic:
simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
  Algebra.id.map_eq_id, RingHom.id_apply, sub_self]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑ₐ (φ a) - a ∈ RingHom.ker ↑φ
⊢ φ a ∈ σ a

Tactic:
simp only [spectrum.mem_iff, ← mem_nonunits_iff,
  coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ φ a ∈ σ a

Tactic:
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
  simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
    Algebra.id.map_eq_id, RingHom.id_apply, sub_self]

Result:
F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑ₐ (φ a) - a ∈ RingHom.ker ↑φ
⊢ φ a ∈ σ a
-- Mathlib/Order/SuccPred/Limit.lean
theorem isMin_or_mem_range_succ_or_isSuccLimit (a) :
    IsMin a ∨ a ∈ range (succ : α → α) ∨ IsSuccLimit a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ IsSuccLimit a

Tactic:
rw [IsSuccLimit]

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
this : a ∈ range succ ∨ IsSuccPrelimit a
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a

Tactic:
have := mem_range_succ_or_isSuccPrelimit a

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
this : a ∈ range succ ∨ IsSuccPrelimit a
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma mu_eq_mu' : (mu 𝕜 : IncidenceAlgebra 𝕜 α) = mu' 𝕜

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ mu 𝕜 = IncidenceAlgebra.mu' 𝕜

Tactic:
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ mu 𝕜 = IncidenceAlgebra.mu' 𝕜

Tactic:
classical
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_isUnit_mul_left_iff {N : Type*} [CommMonoid N] {u a b : N} (hu : IsUnit u) :
    Associated (u * a) b ↔ Associated a b

Proof state:
N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b

Tactic:
exact associated_mul_isUnit_left_iff hu

Result:
no goals

Proof state:
N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ u * a ~ᵤ b ↔ a ~ᵤ b

Tactic:
rw [mul_comm]

Result:
N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top {f : α → ε} (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) (hfp : eLpNorm f p μ < ∞) : ∫⁻ a, ‖f a‖ₑ ^ p.toReal ∂μ < ∞

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : eLpNorm f p μ < ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
apply lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top

Result:
case hq0_lt
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : eLpNorm f p μ < ⊤
⊢ 0 < p.toReal

case hfq
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : eLpNorm f p μ < ⊤
⊢ eLpNorm' f p.toReal μ < ⊤

Proof state:
case hq0_lt
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : eLpNorm f p μ < ⊤
⊢ 0 < p.toReal

Tactic:
exact ENNReal.toReal_pos hp_ne_zero hp_ne_top

Result:
no goals

Proof state:
case hfq
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hfp : eLpNorm f p μ < ⊤
⊢ eLpNorm' f p.toReal μ < ⊤

Tactic:
simpa [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top] using hfp

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
@[simp]
lemma fiberPullbackEquiv_symm_fst_apply {X A B : C} {f : A ⟶ X} {g : B ⟶ X}
    (a : F.obj A) (b : F.obj B) (h : F.map f a = F.map g b) :
    F.map (pullback.fst f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.fst f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

Tactic:
simp [fiberPullbackEquiv]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.fst f g)
      ((PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv
        ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ⟨(a, b), h⟩)) =
    a

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫
        (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.fst f g))
      ⟨(a, b), h⟩ =
    a

Tactic:
erw [PreservesPullback.iso_inv_fst, Types.pullbackIsoPullback_inv_fst]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ F.map (pullback.fst f g)
      ((PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv
        ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ⟨(a, b), h⟩)) =
    a

Tactic:
change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫
  (F ⋙ FintypeCat.incl).map (pullback.fst f g)) _ = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).carrier
b : (F.obj B).carrier
h : F.map f a = F.map g b
⊢ ((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫
        (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.fst f g))
      ⟨(a, b), h⟩ =
    a
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma epi_homologyMap_of_epi_of_not_rel (φ : K ⟶ L) (i : ι)
    [K.HasHomology i] [L.HasHomology i] [Epi (φ.f i)] (hi : ∀ j, ¬ c.Rel i j) :
    Epi (homologyMap φ i) :=
  ((MorphismProperty.epimorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.isoHomologyι i _ rfl (shape _ _ _ (by tauto)))
      (L.isoHomologyι i _ rfl (shape _ _ _ (by tauto))))).2
      (MorphismProperty.epimorphisms.infer_property (opcyclesMap φ i))

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : Epi (φ.f i)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ ¬c.Rel i (c.next i)

Tactic:
tauto

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem smul_support_subset_prod (s : SummableFamily Γ R α)
    (t : SummableFamily Γ' V β) (gh : Γ × Γ') :
    (Function.support fun (i : α × β) ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆
    ((s.finite_co_support' gh.1).prod (t.finite_co_support' gh.2)).toFinset

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
⊢ (Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset

Tactic:
intro _ hab

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : a✝ ∈ Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2
⊢ a✝ ∈ ↑⋯.toFinset

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : ¬(s a✝.1).coeff gh.1 • (t a✝.2).coeff gh.2 = 0
⊢ ¬(s.toFun a✝.1).coeff gh.1 = 0 ∧ ¬(t.toFun a✝.2).coeff gh.2 = 0

Tactic:
exact ⟨left_ne_zero_of_smul hab, right_ne_zero_of_smul hab⟩

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : a✝ ∈ Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2
⊢ a✝ ∈ ↑⋯.toFinset

Tactic:
simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod,
  Set.mem_setOf_eq]

Result:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : ¬(s a✝.1).coeff gh.1 • (t a✝.2).coeff gh.2 = 0
⊢ ¬(s.toFun a✝.1).coeff gh.1 = 0 ∧ ¬(t.toFun a✝.2).coeff gh.2 = 0
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_le_emultiplicity_choose_add {p : ℕ} (hp : p.Prime) :
    ∀ n k : ℕ, emultiplicity p n ≤ emultiplicity p (choose n k) + emultiplicity p k
  | _, 0 => by simp
  | 0, _ + 1 => by simp
  | n + 1, k + 1 => by
    rw [← hp.emultiplicity_mul]
    refine emultiplicity_le_emultiplicity_of_dvd_right ?_
    rw [← succ_mul_choose_eq]
    exact dvd_mul_right _ _

Proof state:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)

Tactic:
rw [← hp.emultiplicity_mul]

Result:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))

Proof state:
p : ℕ
hp : Prime p
x✝ : ℕ
⊢ emultiplicity p x✝ ≤ emultiplicity p (x✝.choose 0) + emultiplicity p 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))

Tactic:
refine emultiplicity_le_emultiplicity_of_dvd_right ?_

Result:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)

Proof state:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ n.succ * n.choose k

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n✝ : ℕ
⊢ emultiplicity p 0 ≤ emultiplicity p (choose 0 (n✝ + 1)) + emultiplicity p (n✝ + 1)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)

Tactic:
rw [← succ_mul_choose_eq]

Result:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ n.succ * n.choose k
-- Mathlib/Topology/Algebra/Monoid.lean
theorem le_nhds_mul (a b : M) : 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Tactic:
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x1 x2 => x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x1 x2 => x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)

Tactic:
exact continuous_mul.tendsto _

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_apply_of_isComplex {w : InfinitePlace K} (hw : IsComplex w) (x : mixedSpace K) :
    normAtPlace w x = ‖x.2 ⟨w, hw⟩‖

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsComplex
x : mixedSpace K
⊢ (normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
  dif_neg (not_isReal_iff_isComplex.mpr hw)]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma pairwiseDisjoint_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) : PairwiseDisjoint (hC.disjointOfDiffUnion hs hI : Set (Set α)) id

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ (↑⋯.choose \ {∅}).PairwiseDisjoint id

Tactic:
exact Set.PairwiseDisjoint.subset
  (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ (↑⋯.choose \ {∅}).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ (↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
classical
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]
exact Set.PairwiseDisjoint.subset
  (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_nfp_iSup (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
    Principal op (nfp (fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2)) o)

Proof state:
case intro.intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
obtain h | h := le_total
  ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[m] o)
  ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[n] o)

Result:
case intro.intro.inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

case intro.intro.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n + 1] o

Tactic:
rw [Function.iterate_succ']

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o
-- Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
theorem toBCF_injective : Function.Injective (toBCF : C₀(α, β) → α →ᵇ β) := fun f g h => by
  ext x
  simpa only using DFunLike.congr_fun h x

Proof state:
case h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
x : α
⊢ f x = g x

Tactic:
simpa only using DFunLike.congr_fun h x

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
⊢ f = g

Tactic:
ext x

Result:
case h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
x : α
⊢ f x = g x
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_mulVec_repr (f : M₁ →ₗ[R] M₂) (x : M₁) :
    LinearMap.toMatrix v₁ v₂ f *ᵥ v₁.repr x = v₂.repr (f x)

Proof state:
case h.e_a.h.e_6.h.h.e_6.h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ v₁.equivFun.symm ⇑(v₁.repr x) = x

Tactic:
exact v₁.equivFun.symm_apply_apply x

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ (v₂.repr (f (v₁.equivFun.symm ⇑(v₁.repr x)))) i = (v₂.repr (f x)) i

Tactic:
congr

Result:
case h.e_a.h.e_6.h.h.e_6.h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ v₁.equivFun.symm ⇑(v₁.repr x) = x

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
⊢ (toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x) = ⇑(v₂.repr (f x))

Tactic:
ext i

Result:
case h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ((toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x)) i = (v₂.repr (f x)) i

Proof state:
case h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ((toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x)) i = (v₂.repr (f x)) i

Tactic:
rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
  LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]

Result:
case h
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ (v₂.repr (f (v₁.equivFun.symm ⇑(v₁.repr x)))) i = (v₂.repr (f x)) i
-- Mathlib/CategoryTheory/Abelian/Exact.lean
/-- A functor which preserves the exactness of short complexes preserves homology. -/
lemma preservesHomology_of_map_exact : L.PreservesHomology where
  preservesCokernels X Y f

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : Mono ((ShortComplex.mk (kernel.ι f) f ⋯).map L).f
⊢ IsLimit (KernelFork.map (Fork.ofι (kernel.ι f) ⋯) L)

Tactic:
exact (hL (ShortComplex.mk _ _ (kernel.condition f))
  (ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel f))).fIsKernel

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : Epi ((ShortComplex.mk f (cokernel.π f) ⋯).map L).g
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L)

Tactic:
exact (hL (ShortComplex.mk _ _ (cokernel.condition f))
  (ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel f))).gIsCokernel

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono ((ShortComplex.mk (kernel.ι f) f ⋯).map L).f

Tactic:
dsimp

Result:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono (L.map (kernel.ι f))
-- Mathlib/RingTheory/PowerBasis.lean
theorem exists_eq_aeval' (pb : PowerBasis R S) (y : S) : ∃ f : R[X], y = aeval pb.gen f

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
⊢ ∃ f, y = (aeval pb.gen) f

Tactic:
obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
f : R[X]
left✝ : f.natDegree < pb.dim
hf : y = (aeval pb.gen) f
⊢ ∃ f, y = (aeval pb.gen) f

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
f : R[X]
left✝ : f.natDegree < pb.dim
hf : y = (aeval pb.gen) f
⊢ ∃ f, y = (aeval pb.gen) f

Tactic:
exact ⟨f, hf⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
⊢ ∃ f, y = (aeval pb.gen) f

Tactic:
nontriviality S

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
⊢ ∃ f, y = (aeval pb.gen) f