harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem select_add_select_not : ∀ x : 𝕎 R, select P x + select (fun i => ¬P i) x = x

Proof state:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i => ¬P i) x) = (ghostComponent n) x

Tactic:
apply_fun aeval x.coeff at this

Result:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  (aeval x.coeff)
      ((bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n)) =
    (aeval x.coeff) (wittPolynomial p ℤ n)
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i => ¬P i) x) = (ghostComponent n) x

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (ghostComponent n) (select P x + select (fun i => ¬P i) x) = (ghostComponent n) x

Tactic:
simp only [RingHom.map_add]

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i => ¬P i) x) = (ghostComponent n) x

Proof state:
case neg
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)

Tactic:
rwa [if_neg Pm, if_pos, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment)
    (assignments0_size : assignments0.size = n) (rupUnits : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (assignments_size : assignments.size = n) (b : Bool)
    (units : CNF.Clause (PosFin n)) :
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) units
    have update_res_size : update_res.snd.fst.size = n

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
h :
  let update_res := insertUnit (rupUnits, assignments, b) hd;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
⊢ InsertUnitInvariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

Tactic:
exact ih update_res.1 update_res.2.1 update_res_size update_res.2.2 h

Result:
no goals

Proof state:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : CNF.Clause (PosFin n)
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ assignments.size = n

Tactic:
exact assignments_size

Result:
no goals
-- Mathlib/Topology/UniformSpace/Matrix.lean
theorem uniformity :
    𝓤 (Matrix m n 𝕜) = ⨅ (i : m) (j : n), (𝓤 𝕜).comap fun a => (a.1 i j, a.2 i j)

Proof state:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap ((fun a => (a.1 i_1, a.2 i_1)) ∘ fun a => (a.1 i, a.2 i)) (𝓤 𝕜) =
    ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (𝓤 (n → 𝕜)) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]

Result:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap ((fun a => (a.1 i_1, a.2 i_1)) ∘ fun a => (a.1 i, a.2 i)) (𝓤 𝕜) =
    ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)

Proof state:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ 𝓤 (Matrix m n 𝕜) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
erw [Pi.uniformity]

Result:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (𝓤 (n → 𝕜)) = ⨅ i, ⨅ j, Filter.comap (fun a => (a.1 i j, a.2 i j)) (𝓤 𝕜)
-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_comp_eq_lintegral_meas_le_mul (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f)
    (f_mble : AEMeasurable f μ) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t)
    (g_nn : ∀ᵐ t ∂volume.restrict (Ioi 0), 0 ≤ g t) :
    ∫⁻ ω, ENNReal.ofReal (∫ t in (0)..f ω, g t) ∂μ =
      ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
case h.e_a
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
t : ℝ
ht : g t = G t
⊢ μ {a | t ≤ f a} = μ {a | t ≤ F a}

Tactic:
apply measure_congr

Result:
case h.e_a.H
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
t : ℝ
ht : g t = G t
⊢ {a | t ≤ f a} =ᶠ[ae μ] {a | t ≤ F a}
-- Mathlib/Data/Set/Function.lean
theorem _root_.Function.invFunOn_image_image_subset [Nonempty α] (f : α → β) (s : Set α) :
    (invFunOn f s) '' (f '' s) ⊆ s

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s

Tactic:
exact invFunOn_apply_mem hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ invFunOn f s '' (f '' s) ⊆ s

Tactic:
rintro _ ⟨_, ⟨x,hx,rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem map_rangeS : f.rangeS.map g = (g.comp f).rangeS

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g f.rangeS = (g.comp f).rangeS

Tactic:
simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean
theorem star_algebraMap (r : R) :
    star (algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ star ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r

Tactic:
rw [star_def, involute.commutes, reverse.commutes]

Result:
no goals
-- Mathlib/RingTheory/Localization/Integer.lean
theorem exist_integer_multiples_of_finite {ι : Type*} [Finite ι] (f : ι → S) :
    ∃ b : M, ∀ i, IsLocalization.IsInteger R ((b : R) • f i)

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f

Result:
case intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : ↥M
hb : ∀ i ∈ Finset.univ, IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : ↥M
hb : ∀ i ∈ Finset.univ, IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Pi.basisFun_det : (Pi.basisFun R ι).det = Matrix.detRowAlternating

Proof state:
case H
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : ι → ι → R
⊢ (basisFun R ι).det M = detRowAlternating M

Tactic:
rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (basisFun R ι).det = detRowAlternating

Tactic:
ext M

Result:
case H
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : ι → ι → R
⊢ (basisFun R ι).det M = detRowAlternating M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem unattach_filter {p : α → Prop} {o : Option { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (o.filter f).unattach = o.unattach.filter g

Proof state:
case some
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
val✝ : { x // p x }
⊢ (Option.filter f (some val✝)).unattach = Option.filter g (some val✝).unattach

Tactic:
simp only [filter_some, hf, unattach_some]

Result:
case some
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
val✝ : { x // p x }
⊢ (if g val✝.val = true then some val✝ else none).unattach = if g val✝.val = true then some val✝.val else none

Proof state:
α : Type u_1
p : α → Prop
o : Option { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (Option.filter f o).unattach = Option.filter g o.unattach

Tactic:
cases o

Result:
case none
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (Option.filter f none).unattach = Option.filter g none.unattach

case some
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
val✝ : { x // p x }
⊢ (Option.filter f (some val✝)).unattach = Option.filter g (some val✝).unattach

Proof state:
case none
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (Option.filter f none).unattach = Option.filter g none.unattach

Tactic:
simp

Result:
no goals

Proof state:
case some
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
val✝ : { x // p x }
⊢ (if g val✝.val = true then some val✝ else none).unattach = if g val✝.val = true then some val✝.val else none

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense. -/
lemma contMDiffAt_vectorSpace_iff_contDiffAt
    {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {n : ℕ∞} {x : E} :
    ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) x ↔
      ContDiffAt 𝕜 n V x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
n : ℕ∞
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (↑n) (fun x => { proj := x, snd := V x }) x ↔ ContDiffAt 𝕜 (↑n) V x

Tactic:
simp only [← contMDiffWithinAt_univ, ← contDiffWithinAt_univ,
  contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_subtypePerm {h} {x y : { x // p x }} :
    (f.subtypePerm h).SameCycle x y ↔ f.SameCycle x y :=
  exists_congr fun n => by simp [Subtype.ext_iff]

Proof state:
α : Type u_2
f : Perm α
p : α → Prop
h : ∀ (x : α), p x ↔ p (f x)
x y : { x // p x }
n : ℤ
⊢ (f.subtypePerm h ^ n) x = y ↔ (f ^ n) ↑x = ↑y

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then the L-series of `f - g` is zero for large real arguments. -/
lemma LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq {f g : ℕ → ℂ}
    (hf : abscissaOfAbsConv f < ⊤) (hg : abscissaOfAbsConv g < ⊤)
    (h : (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] fun x ↦ LSeries g x) :
    (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
⊢ LSeries (f - g) ↑x = 0 x

Tactic:
have Hf : LSeriesSummable f x := by
  refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
    (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
  exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx

Result:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Tactic:
refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ x₀ ⊔ (yf ⊔ yg)
⊢ LSeries (f - g) ↑x = 0 x

Proof state:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

Tactic:
obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf

Result:
case intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
-- Mathlib/Data/Finsupp/Fin.lean
theorem cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ cons y s = 0

Tactic:
rw [h', c, Finsupp.cons_zero_zero]

Result:
no goals

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
⊢ y ≠ 0 ∨ s ≠ 0

Tactic:
refine imp_iff_not_or.1 fun h' c => h ?_

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ cons y s = 0

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Tactic:
refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩

Result:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
⊢ y ≠ 0 ∨ s ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem of_decide_eq_false {p : Prop} {_ : Decidable p} : decide p = false → p = False

Proof state:
p : Prop
x✝ : Decidable p
⊢ decide p = false → p = False

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[ext]
lemma hom_ext₀ {F G : ComposableArrows C 0} {φ φ' : F ⟶ G}
    (h : app' φ 0 = app' φ' 0) :
    φ = φ'

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 ⋯ = app' φ' 0 ⋯
⊢ φ = φ'

Tactic:
ext i

Result:
case w.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 ⋯ = app' φ' 0 ⋯
i : Fin (0 + 1)
⊢ φ.app i = φ'.app i

Proof state:
case w.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 ⋯ = app' φ' 0 ⋯
i : Fin (0 + 1)
⊢ φ.app i = φ'.app i

Tactic:
fin_cases i

Result:
case w.h.«0»
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 ⋯ = app' φ' 0 ⋯
⊢ φ.app ((fun i => i) ⟨0, ⋯⟩) = φ'.app ((fun i => i) ⟨0, ⋯⟩)

Proof state:
case w.h.«0»
C : Type u_1
inst✝ : Category.{u_2, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 ⋯ = app' φ' 0 ⋯
⊢ φ.app ((fun i => i) ⟨0, ⋯⟩) = φ'.app ((fun i => i) ⟨0, ⋯⟩)

Tactic:
exact h

Result:
no goals
-- Mathlib/CategoryTheory/GlueData.lean
theorem t'_inv (i j k : D.J) :
    D.t' i j k ≫ (pullbackSymmetry _ _).hom ≫ D.t' j i k ≫ (pullbackSymmetry _ _).hom = 𝟙 _

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom =
    𝟙 (pullback (D.f i j) (D.f i k))

Tactic:
rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]

Result:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ (D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k) =
    𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j k : D.J
⊢ (D.t' i j k ≫ (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ D.t' j i k ≫ (pullbackSymmetry (D.f i k) (D.f i j)).hom) ≫
      pullback.fst (D.f i j) (D.f i k) =
    𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)

Tactic:
simp [t_fac, t_fac_assoc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α]
    {m : Imp α β} (H : WF m) : WF (mapVal f m)

Proof state:
case refine_1.e_a.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (fun x => x.toList.length) = (fun x => x.toList.length) ∘ AssocList.mapVal f

Tactic:
funext l

Result:
case refine_1.e_a.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
l : AssocList α β
⊢ l.toList.length = ((fun x => x.toList.length) ∘ AssocList.mapVal f) l

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ m.buckets.size = Buckets.size ⟨Array.map (AssocList.mapVal f) m.buckets.val, ⋯⟩

Tactic:
simp only [Buckets.size, Array.toList_map, List.map_map]

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
h₁ : m.size = m.buckets.size
h₂ : m.buckets.WF
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map ((fun x => x.toList.length) ∘ AssocList.mapVal f) m.buckets.val.toList).sum
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem coeff_opRingEquiv (p : R[X]ᵐᵒᵖ) (n : ℕ) :
    (opRingEquiv R p).coeff n = op ((unop p).coeff n)

Proof state:
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ((opRingEquiv R) (op { toFinsupp := toFinsupp✝ })).coeff n = op ((unop (op { toFinsupp := toFinsupp✝ })).coeff n)

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R[X]
⊢ ((opRingEquiv R) (op p)).coeff n = op ((unop (op p)).coeff n)

Tactic:
cases p

Result:
case h.ofFinsupp
R : Type u_1
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ((opRingEquiv R) (op { toFinsupp := toFinsupp✝ })).coeff n = op ((unop (op { toFinsupp := toFinsupp✝ })).coeff n)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ ((opRingEquiv R) p).coeff n = op ((unop p).coeff n)

Tactic:
induction' p with p

Result:
case h
R : Type u_1
inst✝ : Semiring R
n : ℕ
p : R[X]
⊢ ((opRingEquiv R) (op p)).coeff n = op ((unop (op p)).coeff n)