harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
theorem AffineBasis.centroid_mem_interior_convexHull {ι} [Fintype ι] (b : AffineBasis ι ℝ V) :
    Finset.univ.centroid ℝ b ∈ interior (convexHull ℝ (range b))

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
this : Nonempty ι
⊢ Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (range ⇑b))

Tactic:
simp only [b.interior_convexHull, mem_setOf_eq, b.coord_apply_centroid (Finset.mem_univ _),
  inv_pos, Nat.cast_pos, Finset.card_pos, Finset.univ_nonempty, forall_true_iff]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
⊢ Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (range ⇑b))

Tactic:
haveI := b.nonempty

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
this : Nonempty ι
⊢ Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (range ⇑b))
-- Mathlib/CategoryTheory/Localization/Resolution.lean
lemma isIso_iff_of_hasRightResolutions [Φ.HasRightResolutions] {F G : D₂ ⥤ H} (α : F ⟶ G) :
    IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Proof state:
case mpr
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
H : Type u_4
inst✝⁵ : Category.{u_5, u_1} C₁
inst✝⁴ : Category.{u_6, u_2} C₂
inst✝³ : Category.{u_7, u_3} D₂
inst✝² : Category.{u_8, u_4} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
this : ∀ (X₂ : D₂), IsIso (α.app X₂)
⊢ IsIso α

Tactic:
exact NatIso.isIso_of_isIso_app α

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.leadingCoeff_mul_eq_left
    (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hq : q.Monic D) :
    (p * q).leadingCoeff D = p.leadingCoeff D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0

case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Proof state:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
rw [leadingCoeff, hq.supDegree_mul_of_ne_zero_left hD hadd hp,
  apply_supDegree_add_supDegree hD hadd, hq, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Independence.lean
theorem independent_pair_iff_neq (u v : ℙ K V) : Independent ![u, v] ↔ u ≠ v

Proof state:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ Independent ![u, v] ↔ u ≠ v

Tactic:
rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem derivedSeries_le_lowerCentralSeries (k : ℕ) :
    derivedSeries R L k ≤ lowerCentralSeries R L L k

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ derivedSeries R L 0 ≤ lowerCentralSeries R L L 0

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆

Tactic:
exact LieSubmodule.mono_lie h' h

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L k ≤ ⊤

Tactic:
simp only [le_top]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ derivedSeries R L k ≤ lowerCentralSeries R L L k

Tactic:
induction k with
| zero => rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
| succ k h =>
  have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
  rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
  exact LieSubmodule.mono_lie h' h

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)

Tactic:
have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_trunc_of_le {n m} (f : R⟦X⟧) (hnm : n ≤ m

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
⊢ trunc n ↑(trunc m f) = trunc n f

Tactic:
ext d

Result:
case a
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
⊢ (trunc n ↑(trunc m f)).coeff d = (trunc n f).coeff d

Proof state:
case a
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
⊢ (trunc n ↑(trunc m f)).coeff d = (trunc n f).coeff d

Tactic:
rw [coeff_trunc, coeff_trunc, coeff_coe]

Result:
case a
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
⊢ (if d < n then (trunc m f).coeff d else 0) = if d < n then (coeff R d) f else 0

Proof state:
case a
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
⊢ (if d < n then (trunc m f).coeff d else 0) = if d < n then (coeff R d) f else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
h : d < n
⊢ (trunc m f).coeff d = (coeff R d) f

case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
h : ¬d < n
⊢ 0 = 0

Proof state:
case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
h : ¬d < n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : autoParam (n ≤ m) _auto✝
d : ℕ
h : d < n
⊢ (trunc m f).coeff d = (coeff R d) f

Tactic:
rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem eq_singularPart' (t : SignedMeasure α) {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
    t = s.singularPart μ

Proof state:
case e_a.e_μ
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ

Tactic:
have hfneg : Measurable fun x => ENNReal.ofReal (-f x) :=
  (measurable_neg_iff.mpr hf).real_toNNReal.coe_nnreal_ennreal

Result:
case e_a.e_μ
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfneg : Measurable fun x => ENNReal.ofReal (-f x)
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
-- Mathlib/CategoryTheory/Presentable/Basic.lean
lemma isCardinalAccessible_of_natIso [F.IsCardinalAccessible κ] : G.IsCardinalAccessible κ where
  preservesColimitOfShape J _ hκ

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J G

Tactic:
exact preservesColimitsOfShape_of_natIso e

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J G

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J G
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem _root_.not_small_cardinal : ¬ Small.{u} Cardinal.{max u v}

Proof state:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Tactic:
rw [← small_univ_iff, ← bddAbove_iff_small] at this

Result:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False

Proof state:
⊢ ¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}

Tactic:
intro h

Result:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Proof state:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Tactic:
have := small_lift.{_, v} Cardinal.{max u v}

Result:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Proof state:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False

Tactic:
exact not_bddAbove_univ this

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem invFun_add {p q} : invFun R A (p + q) = invFun R A p + invFun R A q

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p q : A[X]
⊢ invFun R A (p + q) = invFun R A p + invFun R A q

Tactic:
simp only [invFun, eval₂_add]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_succ : a ♯ succ b = succ (a ♯ b)

Proof state:
a b : Ordinal.{u}
⊢ a ♯ succ b = succ (a ♯ b)

Tactic:
rw [← nadd_one (a ♯ b), nadd_assoc, nadd_one]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
    s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ l.prod.totalDegree ≤ (List.map totalDegree l).sum

Tactic:
exact totalDegree_list_prod l

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset (MvPolynomial σ R)
⊢ s.prod.totalDegree ≤ (Multiset.map totalDegree s).sum

Tactic:
refine Quotient.inductionOn s fun l => ?_

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ (Multiset.prod ⟦l⟧).totalDegree ≤ (Multiset.map totalDegree ⟦l⟧).sum

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ (Multiset.prod ⟦l⟧).totalDegree ≤ (Multiset.map totalDegree ⟦l⟧).sum

Tactic:
rw [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe, Multiset.sum_coe]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ l.prod.totalDegree ≤ (List.map totalDegree l).sum
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoInitial_hom [HasInitial C] : zeroIsoInitial.hom = (0 : 0 ⟶ ⊥_ C)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.hom = 0

Tactic:
ext

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem domRestrict_apply {f : E →ₗ.[R] F} {S : Submodule R E} ⦃x : ↥(S ⊓ f.domain)⦄ ⦃y : f.domain⦄
    (h : (x : E) = y) : f.domRestrict S x = f y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ S ⊓ f.domain ≤ f.domain

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑(f.domRestrict S) x = ↑f y

Tactic:
have : Submodule.inclusion (by simp) x = y := by
  ext
  simp [h]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f y

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f ((Submodule.inclusion ⋯) x)

Tactic:
exact LinearPMap.mk_apply _ _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f y

Tactic:
rw [← this]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f ((Submodule.inclusion ⋯) x)

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ (Submodule.inclusion ⋯) x = y

Tactic:
ext

Result:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑((Submodule.inclusion ⋯) x) = ↑y

Proof state:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑((Submodule.inclusion ⋯) x) = ↑y

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_norm_eq (n : ℕ) :
    ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖F.eval (newton_seq n)‖ / ‖F.derivative.eval (newton_seq n)‖

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖↑⟨↑(newton_seq_aux hnorm n) -
              ⟨↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                  ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)),
                ⋯⟩,
            ⋯⟩ -
        ↑(newton_seq_aux hnorm n)‖ =
    ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) F‖ /
      ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖

Tactic:
simp [sub_eq_add_neg, add_comm]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (Polynomial.derivative F)‖

Tactic:
rw [newton_seq_gen, newton_seq_gen, newton_seq_aux, ih_n]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖↑⟨↑(newton_seq_aux hnorm n) -
              ⟨↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                  ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)),
                ⋯⟩,
            ⋯⟩ -
        ↑(newton_seq_aux hnorm n)‖ =
    ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) F‖ /
      ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_const' (μ : Measure α) (c : ℝ) :
    μ.tilted (fun _ ↦ c) = (μ Set.univ)⁻¹ • μ

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ (μ.tilted fun x => c) = (μ Set.univ)⁻¹ • μ

Tactic:
simp only [Measure.tilted, withDensity_const, integral_const, smul_eq_mul]

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Tactic:
congr

Result:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) = (μ Set.univ)⁻¹

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Tactic:
simp only [h_univ, ENNReal.top_toReal, zero_mul, log_zero, div_zero, ENNReal.ofReal_zero,
  zero_smul, ENNReal.inv_top]

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (Measure.tilted 0 fun x => c) = (0 Set.univ)⁻¹ • 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (μ.tilted fun x => c) = (μ Set.univ)⁻¹ • μ

Tactic:
rw [h]

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (Measure.tilted 0 fun x => c) = (0 Set.univ)⁻¹ • 0

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Tactic:
by_cases h_univ : μ Set.univ = ∞

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Proof state:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ ENNReal.ofReal (rexp c / ((μ Set.univ).toReal * rexp c)) = (μ Set.univ)⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀ (exp_pos _).ne', mul_one,
  ← ENNReal.toReal_inv, ENNReal.ofReal_toReal]

Result:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ (μ Set.univ)⁻¹ ≠ ⊤

Proof state:
case neg.e_a
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ⊤
⊢ (μ Set.univ)⁻¹ ≠ ⊤

Tactic:
simp [h0.out]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma ι_fst : ι f g ≫ biprod.fst = kernel.ι (f ≫ g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ biprod.fst = kernel.ι (f ≫ g)

Tactic:
simp [ι]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma zmod_injective : Injective (zmod n)

Proof state:
n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
hn : ↑n ≠ 0
⊢ ↑x = ↑y

Tactic:
simpa [pi_ne_zero, exp_inj, hn, CharP.intCast_eq_intCast (ZMod n) n] using
  (zmod_intCast ..).symm.trans <| (DFunLike.congr_fun h ((1 : ℤ) : ZMod n)).trans <|
    zmod_intCast ..

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ∀ (x x_1 : ℤ), zmod n ↑x = zmod n ↑x_1 → ↑x = ↑x_1

Tactic:
rintro x y h

Result:
n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
⊢ ↑x = ↑y

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ Injective (zmod n)

Tactic:
simp_rw [Injective, ZMod.intCast_surjective.forall]

Result:
n : ℕ
inst✝ : NeZero n
⊢ ∀ (x x_1 : ℤ), zmod n ↑x = zmod n ↑x_1 → ↑x = ↑x_1

Proof state:
n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
⊢ ↑x = ↑y

Tactic:
have hn : (n : ℝ) ≠ 0 := NeZero.ne _

Result:
n : ℕ
inst✝ : NeZero n
x y : ℤ
h : zmod n ↑x = zmod n ↑y
hn : ↑n ≠ 0
⊢ ↑x = ↑y
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem not_cliqueFree_card_of_top_embedding [Fintype α] (f : (⊤ : SimpleGraph α) ↪g G) :
    ¬G.CliqueFree (card α)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ ¬G.CliqueFree (Fintype.card α)

Tactic:
rw [not_cliqueFree_iff]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ Nonempty (⊤ ↪g G)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : ⊤ ↪g G
⊢ Nonempty (⊤ ↪g G)

Tactic:
exact ⟨(Iso.completeGraph (Fintype.equivFin α)).symm.toEmbedding.trans f⟩

Result:
no goals