harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem measure_limRatioMeas_top : μ {x | v.limRatioMeas hρ x = ∞} = 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 0)
⊢ μ s ≤ 0

Tactic:
apply ge_of_tendsto B

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop, μ s ≤ (↑c)⁻¹ * ρ s

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ μ s ≤ (↑q)⁻¹ * ρ s

Tactic:
rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q * μ s ≤ ρ s

α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q ≠ 0 ∨ ρ s ≠ 0
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem pow_mem_ball {n : ℕ} (hn : 0 < n) (h : a ∈ ball b r) : a ^ n ∈ ball (b ^ n) (n • r)

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < n • r

Tactic:
rw [nsmul_eq_mul]

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < ↑n * r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < ↑n * r

Tactic:
nlinarith

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ↑n * ‖a / b‖ < n • r

Tactic:
replace hn : 0 < (n : ℝ) := by norm_cast

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a / b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a / b‖ < n • r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ‖(a / b) ^ n‖ < n • r

Tactic:
refine lt_of_le_of_lt norm_pow_le_mul_norm ?_

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ↑n * ‖a / b‖ < n • r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
⊢ a ^ n ∈ ball (b ^ n) (n • r)

Tactic:
simp only [mem_ball, dist_eq_norm_div, ← div_pow] at h ⊢

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a / b‖ < r
⊢ ‖(a / b) ^ n‖ < n • r
-- Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
theorem exists_approx_aux (n : ℕ) (h : abv.IsAdmissible) :
    ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
      ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ k, (abv (A i₁ k % b - A i₀ k % b) : ℝ) < abv b • ε

Proof state:
case intro.intro.refine_3
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < (Finset.filter (fun x => t x = s) Finset.univ).card
i₀ i₁ : Fin (M ^ n).succ
this :
  ∀ (i : ℕ) (h : i < (Finset.filter (fun x => t x = s) Finset.univ).toList.length),
    t ((Finset.filter (fun x => t x = s) Finset.univ).toList.get ⟨i, h⟩) = s
⊢ t ((fun i => (Finset.filter (fun x => t x = s) Finset.univ).toList.get (Fin.castLE ⋯ i)) i₀) =
    t ((fun i => (Finset.filter (fun x => t x = s) Finset.univ).toList.get (Fin.castLE ⋯ i)) i₁)

Tactic:
simp only [Nat.succ_eq_add_one, Finset.length_toList, List.get_eq_getElem] at this

Result:
case intro.intro.refine_3
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < (Finset.filter (fun x => t x = s) Finset.univ).card
i₀ i₁ : Fin (M ^ n).succ
this :
  ∀ (i : ℕ) (h : i < (Finset.filter (fun x => t x = s) Finset.univ).card),
    t (Finset.filter (fun x => t x = s) Finset.univ).toList[i] = s
⊢ t ((fun i => (Finset.filter (fun x => t x = s) Finset.univ).toList.get (Fin.castLE ⋯ i)) i₀) =
    t ((fun i => (Finset.filter (fun x => t x = s) Finset.univ).toList.get (Fin.castLE ⋯ i)) i₁)
-- Mathlib/Data/Nat/PrimeFin.lean
lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
    (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

Proof state:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a.gcd b).primeFactors ↔ a✝ ∈ a.primeFactors ∩ b.primeFactors

Tactic:
simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]

Result:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ Prime a✝ ∧ a✝ ∣ a ∧ a✝ ∣ b ↔ (Prime a✝ ∧ a✝ ∣ a) ∧ Prime a✝ ∧ a✝ ∣ b

Proof state:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ Prime a✝ ∧ a✝ ∣ a ∧ a✝ ∣ b ↔ (Prime a✝ ∧ a✝ ∣ a) ∧ Prime a✝ ∧ a✝ ∣ b

Tactic:
aesop

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

Tactic:
ext

Result:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a.gcd b).primeFactors ↔ a✝ ∈ a.primeFactors ∩ b.primeFactors
-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem isIntegral (hpos : 0 < n) : IsIntegral ℤ μ

Proof state:
case h.right
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0

Tactic:
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
  sub_self]

Result:
no goals

Proof state:
case h
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0

Tactic:
constructor

Result:
case h.left
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (X ^ n - 1).Monic

case h.right
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0

Proof state:
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ IsIntegral ℤ μ

Tactic:
use X ^ n - 1

Result:
case h
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0

Proof state:
case h.left
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (X ^ n - 1).Monic

Tactic:
exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd_inv_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
    ((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_comm a, add_assoc])).hom := rfl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + b + a = n + (a + b)

Tactic:
rw [add_comm a, add_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + { as := b }.as + { as := a }.as = n + { as := a + b }.as

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + b + a = n + (a + b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_toList (p : α → Bool) (v : Vector α n) :
    v.toList.all p = v.all p

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ v.toList.all p = v.all p

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.all p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.all p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList.all p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.all p

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_iff_isSheaf_comp (s : A ⥤ B) [HasLimitsOfSize.{v₁, max v₁ u₁} A]
    [PreservesLimitsOfSize.{v₁, max v₁ u₁} s] [s.ReflectsIsomorphisms] :
    IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst✝ : s.ReflectsIsomorphisms
this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := reflectsLimits_of_reflectsIsomorphisms
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
exact ⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst✝ : s.ReflectsIsomorphisms
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
letI : ReflectsLimitsOfSize s := reflectsLimits_of_reflectsIsomorphisms

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst✝ : s.ReflectsIsomorphisms
this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := reflectsLimits_of_reflectsIsomorphisms
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma ker_π : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
simpa only [← injective_fromQuotient_iff_ker_π_eq_span] using h.bijective.1

Result:
no goals
-- Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean
lemma hom_ext {Z : C} {φ₁ φ₂ : Y ⟶ Z} (h₀ : f ≫ φ₁ = f ≫ φ₂)
    (h : ∀ (γ : Cells c), γ.ι ≫ φ₁ = γ.ι ≫ φ₂) :
    φ₁ = φ₂

Proof state:
case hm
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : IsMin j
⊢ c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂

Tactic:
obtain rfl := hj.eq_bot

Result:
case hm
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
hj : IsMin ⊥
⊢ c.incl.app ⊥ ≫ φ₁ = c.incl.app ⊥ ≫ φ₂

Proof state:
case hs.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : ¬IsMax j
hj' : c.incl.app j ≫ φ₁ = c.incl.app j ≫ φ₂
i : (c.attachCells j hj).ι
⊢ (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells j hj).cell i ≫ c.incl.app (Order.succ j) ≫ φ₂

Tactic:
simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i })

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_union_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
    Ico a b ∪ Ico b c = Ico a c

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_apply_ne_self_iff {a b x : α} : swap a b x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Proof state:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : x = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
simp [hbx]

Result:
no goals

Proof state:
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : ¬x = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
simp [hab, hax, hbx, swap_apply_of_ne_of_ne]

Result:
no goals

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
by_cases hab : a = b

Result:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : a = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Proof state:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : x = a
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
simp [hax, eq_comm]

Result:
no goals

Proof state:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : a = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
simp [hab]

Result:
no goals

Proof state:
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
by_cases hbx : x = b

Result:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : x = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : ¬x = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Proof state:
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
by_cases hax : x = a

Result:
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : x = a
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem update_insertNth (p : Fin (n + 1)) (x y : α p) (f : ∀ i, α (p.succAbove i)) :
    update (p.insertNth x f) p y = p.insertNth y f

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : α p
f : (i : Fin n) → α (p.succAbove i)
i : Fin (n + 1)
⊢ update (p.insertNth x f) p y i = p.insertNth y f i

Tactic:
cases i using p.succAboveCases <;> simp [succAbove_ne]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ update (p.insertNth x f) p y = p.insertNth y f

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : α p
f : (i : Fin n) → α (p.succAbove i)
i : Fin (n + 1)
⊢ update (p.insertNth x f) p y i = p.insertNth y f i
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.tendsto_atBot_zero (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν]
    (a : α) :
    ∀ᵐ t ∂(ν a), Tendsto (f (a, t)) atBot (𝓝 0)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
rw [h_eq_neg]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
⊢ Tendsto (fun q => f (a, t) (- -q)) atBot (𝓝 0)
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem map_nonneg (ha : 0 ≤ a) : 0 ≤ f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rw [← map_zero f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ f 0 ≤ f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ f 0 ≤ f a

Tactic:
exact OrderHomClass.mono _ ha

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac
    {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} (f₃ : F₁ ⟶ F₃) (fac : f₁ ≫ f₂ = f₃)
    [IsLocallyInjective J f₃] [IsLocallySurjective J f₁] :
    IsLocallyInjective J f₂

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝¹ : IsLocallyInjective J f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallyInjective J f₂

Tactic:
subst fac

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J f₁
inst✝ : IsLocallyInjective J (f₁ ≫ f₂)
⊢ IsLocallyInjective J f₂

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J f₁
inst✝ : IsLocallyInjective J (f₁ ≫ f₂)
⊢ IsLocallyInjective J f₂

Tactic:
exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem support_powerSeriesFamily_subset (hx : 0 < x.orderTop) (a b : PowerSeries R) (g : Γ) :
    ((powerSeriesFamily hx (a * b)).coeff g).support ⊆
    (((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).coeff g).support.image
      fun i => i.1 + i.2

Proof state:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ ↑⋯.toFinset ∧ a_1 + b_1 = n

Tactic:
use he.choose.1, he.choose.2

Result:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ (he.choose.1, he.choose.2) ∈ ↑⋯.toFinset ∧ he.choose.1 + he.choose.2 = n

Proof state:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ (he.choose.1, he.choose.2) ∈ ↑⋯.toFinset

Tactic:
simp only [mul_toFun, smulFamily_toFun, powers_toFun, Algebra.mul_smul_comm,
  Algebra.smul_mul_assoc, HahnSeries.coeff_smul, Set.Finite.coe_toFinset, ne_eq, Prod.mk.eta,
  Function.mem_support]

Result:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
a b : PowerSeries R
g : Γ
n : ℕ
hn :
  ∑ x_1 ∈ antidiagonal n, (PowerSeries.coeff R x_1.1) a • (PowerSeries.coeff R x_1.2) b • ((powers x hx) n).coeff g ≠ 0
he : ∃ a_1, a_1.1 + a_1.2 = n ∧ (PowerSeries.coeff R a_1.1) a • (PowerSeries.coeff R a_1.2) b • (x ^ n).coeff g ≠ 0
⊢ ¬(PowerSeries.coeff R he.choose.2) b •
        (PowerSeries.coeff R he.choose.1) a • (x ^ he.choose.1 * x ^ he.choose.2).coeff g =
      0