mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ (∫⁻ (x : ℝ), gammaPDF a r x).toReal = 1

Tactic:
← lintegral_add_compl _ measurableSet_Ici,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.155, gammaPDF a r x) + ∫⁻ (x : ℝ) in (Ici ?m.155)ᶜ, gammaPDF a r x).toReal = 1

a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ℝ
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
x : α
⊢ p.toMeasure {x} = q x

Tactic:
← q.toMeasure_apply_singleton x <| measurableSet_singleton x,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
x : α
⊢ p.toMeasure {x} = q.toMeasure {x}
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Goal state after:
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ (∫⁻ (x : ℝ), paretoPDF t r x).toReal = 1

Tactic:
← lintegral_add_compl _ measurableSet_Ici,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.111, paretoPDF t r x) + ∫⁻ (x : ℝ) in (Ici ?m.111)ᶜ, paretoPDF t r x).toReal = 1

t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ℝ
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ b ∈ ⋃ a ∈ p.support, (f a).support

Tactic:
by simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bernoulli p h) b = ↑(bif b then p else 1 - p)

Tactic:
simp only [bernoulli, ofFintype_apply]

Goal state after:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bif b then ↑p else 1 - ↑p) = ↑(bif b then p else 1 - p)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
have hf₂ : Measurable (Prod.fst : X × PUnit → X) := by fun_prop

Goal state after:
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
have h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ := by
        apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
        · exact Measurable.stronglyMeasurable <|
            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
        · exact integrable_stoppedValue ι hτ h.integrable hτ_le

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Var[X; μ.tilted fun x ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t

Tactic:
rw [variance_eq_integral]
  swap; · exact (memLp_tilted_mul ht 1).aestronglyMeasurable.aemeasurable
  rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf,
    ← integral_div]
  simp only [smul_eq_mul]
  congr with ω
  ring

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') Set.univ ≤ 1

Tactic:
filter_upwards [h.isFiniteMeasure, h.mgf_le] with ω' h h_mgf

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (κ ω') Set.univ ≤ 1
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : MonoidAlgebra.single g 1 • w ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
Representation.single_smul,

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : 1 • (ρ g) (ρ.asModuleEquiv w) ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
⊢ (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ (ρ.tprod τ) x =
    (σ.tprod π) x ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
by
    rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ g) (ρ.averageMap v) = ρ.averageMap v

Tactic:
averageMap,

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ g) ((ρ.asAlgebraHom (average k G)) v) = (ρ.asAlgebraHom (average k G)) v
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
ι : Type u'
f : ι → (A ⟶ B)
s : Finset ι
⊢ Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
⊢ ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

Tactic:
rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h

Goal state after:
case inl
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g : G
a : ↑A
s s₁ : ↥S
⊢ (A.indToCoindAux g) a (↑s * (fun m ↦ m • g) s₁) = (A.ρ s) ((A.indToCoindAux g) a ((fun m ↦ m • g) s₁))

case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap = d k G (n + 1)

Tactic:
refine MonoidAlgebra.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : Fin (n + 2) → G
⊢ ((Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x) 1 =
    (d k G (n + 1) ∘ₗ MonoidAlgebra.lsingle x) 1
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ f ∈ cocycles₂ A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

Tactic:
simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
    add_comm (f (_ * _, _))]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤
    (map I ((lsum R) fun i ↦ ↑i • LinearMap.id) ∘ₗ map I ↑(finsuppLEquivDirectSum R M ↥s).symm).range

Tactic:
LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top_of_surjective _ <|
      Function.RightInverse.surjective (g := map I (finsuppLEquivDirectSum R M s)) (fun _ ↦ by
      simp [← LinearMap.comp_apply, map_comp]))

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
⊢ (ofPowSMul I M n).range ≤ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)).range
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
m n : ℕ
h' : m ≤ n
⊢ (transitionMap I M h') ((fun i ↦ ↑(x i) i) n) = (fun i ↦ ↑(x i) i) m

Tactic:
by
        simp only [transitionMap_comp_eval_apply]
        specialize hx h'
        rwa [SModEq.sub_mem, pow_smul_top_eq_ker_eval h, LinearMap.mem_ker, _root_.map_sub,
          sub_eq_zero, eval_apply, eval_apply, eq_comm] at hx

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by
    have h : (Algebra.TensorProduct.comm R (SymmetricAlgebra R M)
          (SymmetricAlgebra R M)).toAlgHom.comp (Bialgebra.comulAlgHom R _) =
        Bialgebra.comulAlgHom R (SymmetricAlgebra R M) := by
      ext x
      simp
      abel
    exact congr(($h).toLinearMap)

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : IsDedekindDomain A
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ mk0 (extendedIdeal B C (extendedIdeal A B I)) = (extendedHom A C) (mk0 I)

Tactic:
extendedHom_mk0 A C I,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : IsDedekindDomain A
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ mk0 (extendedIdeal B C (extendedIdeal A B I)) = mk0 (extendedIdeal A C I)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
p q : R[X]
⊢ ∀ b ∈ {J | (p * q).contentIdeal ≤ J ∧ J.IsPrime}, p.contentIdeal * q.contentIdeal ≤ b

Tactic:
intro P ⟨hpq, hPprime⟩

Goal state after:
R : Type u_3
inst✝ : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
⊢ p.contentIdeal * q.contentIdeal ≤ P
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    (if ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 = 0 then 0
      else
        exp
          (-↑((Associates.mk v.asIdeal).count
                (Associates.mk (Ideal.span {((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1})).factors))) *
      (if (SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2 = 0 then 0
        else
          exp
            (-↑((Associates.mk v.asIdeal).count
                  (Associates.mk
                      (Ideal.span
                        {(SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2})).factors)))⁻¹

Tactic:
simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
⊢ valuation.ker = selmerGroup.subgroupOf selmerGroup

Tactic:
ext ⟨_, hx⟩

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker ↔ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case H
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := ⋯
p' : PrimeSpectrum R := ⋯
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := ⋯
Nₚ : Type (max u_1 u_3) := ⋯
Mₚ : Type (max u_1 u_2) := ⋯
Nₚ' : Type (max u_1 u_3) := ⋯
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := ⋯
x✝ : Module p.ResidueField Nₚ' := ⋯
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField := ⋯
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := ⋯
hx :
  maximalIdeal (Localization.AtPrime p) = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker
i : p.ResidueField →ₗ[Rₚ] Mₚ := ⋯
inj1 : Function.Injective ⇑i
f : Nₚ →ₗ[Rₚ] Mₚ := ⋯
eq0 : f = 0
np : Nₚ
⊢ i (to_res np) = i 0

Tactic:
change f np = _

Goal state after:
case H
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
hx :
  maximalIdeal (Localization.AtPrime p) = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective ⇑i
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
eq0 : f = 0
np : Nₚ
⊢ f np = i 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(multinomial s n) * hI.dpow (s.sum n) a

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
n : ι → ℕ
m : M
⊢ ∏ i ∈ s, dp R (n i) m = ↑(multinomial s n) * dp R (s.sum n) m

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ Subalgebra.map (RingCon.mkₐ R (ringCon R N)) ⊤ ≤ Subalgebra.map (map R f) ⊤

Tactic:
(Subalgebra.gc_map_comap _).le_iff_le,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ⊤ ≤ Subalgebra.comap (RingCon.mkₐ R (ringCon R N)) (Subalgebra.map (map R f) ⊤)