harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
    (s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X))
    (i : I) (f : LocallyConstant (toProfinite.obj (F.obj i)) X) :
    (isColimitLocallyConstantPresheaf c X hc).desc s (f.comap (c.π.app i).hom) = s.ι.app ⟨i⟩ f

Proof state:
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) f) =
    s.ι.app (Opposite.op i) f

Tactic:
change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨i⟩) ≫
  (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _

Result:
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i) ≫
        (isColimitLocallyConstantPresheaf c X hc).desc s)
      f =
    s.ι.app (Opposite.op i) f

Proof state:
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i) ≫
        (isColimitLocallyConstantPresheaf c X hc).desc s)
      f =
    s.ι.app (Opposite.op i) f

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem toMatrix_inv_vecMul_toMatrix (x : P) :
    b.coords x ᵥ* (b.toMatrix b₂)⁻¹ = b₂.coords x

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂)
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
rw [Matrix.isUnit_iff_isUnit_det] at hu

Result:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
  Matrix.vecMul_one]

Result:
no goals

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
have hu := b.isUnit_toMatrix b₂

Result:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂)
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal × Ordinal} :
    x ∈ CNF b o → x.2 < b

Proof state:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.2 < b

Tactic:
intro h

Result:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.2 < b

Proof state:
case refine_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).2 < b
h : (log b o, o / b ^ log b o) ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).2 < b

Tactic:
exact div_opow_log_lt o hb

Result:
no goals

Proof state:
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b

Tactic:
refine CNFRec b ?_ (fun o ho IH ↦ ?_) o

Result:
case refine_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.2 < b

case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Proof state:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
obtain rfl | h := mem_cons.mp h

Result:
case refine_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).2 < b
h : (log b o, o / b ^ log b o) ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).2 < b

case refine_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Proof state:
case refine_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
exact IH h

Result:
no goals

Proof state:
case refine_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.2 < b

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
rw [CNF_ne_zero ho]

Result:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.2 < b
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem IsCompact.measure_closure [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : Measure γ) :
    μ (closure K) = μ K

Proof state:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ μ (closure K) ≤ μ K

Tactic:
calc
  μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
    hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
  _ = μ K := measure_toMeasurable ..

Result:
no goals

Proof state:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ μ (closure K) = μ K

Tactic:
refine le_antisymm ?_ (measure_mono subset_closure)

Result:
γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ μ (closure K) ≤ μ K
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerRight_iff {X Y : C} (f g : X ⟶ Y) : f ▷ 𝟙_ C = g ▷ 𝟙_ C ↔ f = g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ f ▷ 𝟙_ C = g ▷ 𝟙_ C ↔ f = g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma eq_mul_div_of_mul_eq_mul_of_dvd_left (hb : b ≠ 0) (hbc : b ∣ c) (h : b * a = c * d) :
    a = c / b * d

Proof state:
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d

Tactic:
obtain ⟨k, rfl⟩ := hbc

Result:
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d

Proof state:
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d

Tactic:
rwa [Int.mul_assoc, Int.mul_eq_mul_left_iff hb] at h

Result:
no goals

Proof state:
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d

Tactic:
rw [Int.mul_ediv_cancel_left _ hb]

Result:
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_add_one [LeftDistribClass α] (a b : α) : a * (b + 1) = a * b + a

Proof state:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a

Tactic:
rw [mul_add, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top {ι} [Nonempty ι] [Countable ι]
    [LinearOrder ι] {f : ι → α → F} {f_lim : α → F}
    (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm f_lim ∞ μ ≤ atTop.liminf fun n => eLpNorm (f n) ∞ μ

Proof state:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
ι : Type u_7
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → F
f_lim : α → F
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n => essSup (fun x => ‖f n x‖ₑ) μ) atTop

Tactic:
exact ENNReal.essSup_liminf_le _

Result:
no goals

Proof state:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
ι : Type u_7
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → F
f_lim : α → F
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim ⊤ μ ≤ liminf (fun n => eLpNorm (f n) ⊤ μ) atTop

Tactic:
rw [eLpNorm_exponent_top_lim_eq_essSup_liminf h_lim]

Result:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
ι : Type u_7
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → F
f_lim : α → F
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n => eLpNorm (f n) ⊤ μ) atTop

Proof state:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
ι : Type u_7
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → F
f_lim : α → F
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n => eLpNorm (f n) ⊤ μ) atTop

Tactic:
simp_rw [eLpNorm_exponent_top, eLpNormEssSup]

Result:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
ι : Type u_7
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → F
f_lim : α → F
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n => essSup (fun x => ‖f n x‖ₑ) μ) atTop
-- Mathlib/Algebra/Polynomial/Div.lean
theorem div_wf_lemma (h : degree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
    degree (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) < degree p :=
  have hp : leadingCoeff p ≠ 0 := mt leadingCoeff_eq_zero.1 h.2
  have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne h.2
  have hlt : natDegree q ≤ natDegree p :=
    (Nat.cast_le (α := WithBot ℕ)).1
      (by rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1)
  degree_sub_lt
    (by
      rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt])
    h.2 (by rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C])

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).leadingCoeff

Tactic:
rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ ↑q.natDegree ≤ ↑p.natDegree

Tactic:
rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree

Tactic:
rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
  degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Tactic:
exact h.1

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_list_prod_noncomm (ps : List R[X])
    (hf : ∀ p ∈ ps, ∀ (k), Commute (f <| coeff p k) x) :
    eval₂ f x ps.prod = (ps.map (Polynomial.eval₂ f x)).prod

Proof state:
case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute (f (p_1.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
simp only [List.forall_mem_append, List.forall_mem_singleton] at hf

Result:
case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute (f (x_1.coeff k)) x) ∧ ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Proof state:
case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute (f (x_1.coeff k)) x) ∧ ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod

Tactic:
induction' ps using List.reverseRecOn with ps p ihp

Result:
case nil
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ p ∈ [], ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x [].prod = (List.map (eval₂ f x) []).prod

case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute (f (p_1.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Proof state:
case nil
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ p ∈ [], ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x [].prod = (List.map (eval₂ f x) []).prod

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
lemma map_obj_injective {X Y : C} (f : X ⟶ Y) [Mono f] :
    Function.Injective (Subobject.map f).obj

Proof state:
case h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
X₁ : C
i₁ : X₁ ⟶ X
inst✝¹ : Mono i₁
X₂ : C
i₂ : X₂ ⟶ X
inst✝ : Mono i₂
h : mk (i₁ ≫ f) = mk (i₂ ≫ f)
⊢ mk i₁ = mk i₂

Tactic:
exact mk_eq_mk_of_comm _ _ (isoOfMkEqMk _ _ h) (by simp [← cancel_mono f])

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ Function.Injective (map f).obj

Tactic:
intro X₁ X₂ h

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
X₁ X₂ : Subobject X
h : (map f).obj X₁ = (map f).obj X₂
⊢ X₁ = X₂

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
X₁ : C
i₁ : X₁ ⟶ X
inst✝¹ : Mono i₁
X₂ : C
i₂ : X₂ ⟶ X
inst✝ : Mono i₂
h : mk (i₁ ≫ f) = mk (i₂ ≫ f)
⊢ (isoOfMkEqMk (i₁ ≫ f) (i₂ ≫ f) h).hom ≫ i₂ = i₁

Tactic:
simp [← cancel_mono f]

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
X₂ : Subobject X
X₁ : C
i₁ : X₁ ⟶ X
inst✝ : Mono i₁
h : (map f).obj (mk i₁) = (map f).obj X₂
⊢ mk i₁ = X₂

Tactic:
induction' X₂ using Subobject.ind with X₂ i₂ _

Result:
case h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
X₁ : C
i₁ : X₁ ⟶ X
inst✝¹ : Mono i₁
X₂ : C
i₂ : X₂ ⟶ X
inst✝ : Mono i₂
h : (map f).obj (mk i₁) = (map f).obj (mk i₂)
⊢ mk i₁ = mk i₂

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
X₁ X₂ : Subobject X
h : (map f).obj X₁ = (map f).obj X₂
⊢ X₁ = X₂

Tactic:
induction' X₁ using Subobject.ind with X₁ i₁ _

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
X₂ : Subobject X
X₁ : C
i₁ : X₁ ⟶ X
inst✝ : Mono i₁
h : (map f).obj (mk i₁) = (map f).obj X₂
⊢ mk i₁ = X₂

Proof state:
case h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
X₁ : C
i₁ : X₁ ⟶ X
inst✝¹ : Mono i₁
X₂ : C
i₂ : X₂ ⟶ X
inst✝ : Mono i₂
h : (map f).obj (mk i₁) = (map f).obj (mk i₂)
⊢ mk i₁ = mk i₂

Tactic:
simp only [map_mk] at h

Result:
case h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
X₁ : C
i₁ : X₁ ⟶ X
inst✝¹ : Mono i₁
X₂ : C
i₂ : X₂ ⟶ X
inst✝ : Mono i₂
h : mk (i₁ ≫ f) = mk (i₂ ≫ f)
⊢ mk i₁ = mk i₂
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.add_antiperiod [AddGroup α] [Neg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) :
    Antiperiodic f (c₁ + c₂)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : Neg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem lookupFinsupp_support [DecidableEq α] [DecidableEq M] (l : AList fun _x : α => M) :
    l.lookupFinsupp.support = (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset

Proof state:
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset =
    (filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ l.lookupFinsupp.support = (filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset

Tactic:
dsimp only [lookupFinsupp]

Result:
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset =
    (filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.tendstoUniformlyOn {r' : ℝ≥0}
    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
    TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
      ((x + ·)⁻¹' (insert x s) ∩ Metric.ball (0 : E) r')

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ x_1 ∈ (fun x_2 => x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 ↑r', dist (f (x + x_1)) (p.partialSum n x_1) < ε

Tactic:
refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r'
⊢ dist (f (x + y)) (p.partialSum n y) < ε

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (fun n => C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r'
⊢ ‖f (x + y) - p.partialSum n y‖ < ε

Tactic:
exact (hp y hy.2 n hy.1).trans_lt hn

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem not_congr (w : Nat) (x x' : BitVec w) (h : x = x') : ~~~x' = ~~~x

Proof state:
w : Nat
x x' : BitVec w
h : x = x'
⊢ ~~~x' = ~~~x

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem idealOfSet_closed [T2Space R] (s : Set X) :
    IsClosed (idealOfSet R s : Set C(X, R))

Proof state:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed ↑(idealOfSet R s)

Tactic:
simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]

Result:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed ↑{ carrier := ⋂ i ∈ sᶜ, {x | x i = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

Proof state:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
s : Set X
⊢ IsClosed ↑{ carrier := ⋂ i ∈ sᶜ, {x | x i = 0}, add_mem' := ⋯, zero_mem' := ⋯ }

Tactic:
exact isClosed_iInter fun x => isClosed_iInter fun _ =>
  isClosed_eq (continuous_eval_const x) continuous_const

Result:
no goals