mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ

Tactic:
rw [h1, h2]

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
      Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), cgf X (κ ω') t ≤ ↑c * t ^ 2 / 2

Tactic:
filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul] with ω' h h_int t
  calc cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) (⇑κ ∘ₘ ν)

Tactic:
have h1 := h.integrable_exp_mul t

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (⇑(κ.map Y) ∘ₘ ν)
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) (⇑κ ∘ₘ ν)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
⊢ ∀ᵐ (ω : Ω) ∂P, Monotone fun x ↦ (τ ⊓ σ) x ω

Tactic:
by filter_upwards [hτ.mono, hσ.mono] with ω hτω hσω using hτω.min hσω

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ f x

Tactic:
· calc
      truncation f A x ≤ |truncation f A x| := le_abs_self _
      _ ≤ |f x| := abs_truncation_le_abs_self _ _ _
      _ = f x := abs_of_nonneg (h'f x)

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF X c (Measure.map Y μ)
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) μ

Tactic:
have h1 := h.integrable_exp_mul t

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF X c (Measure.map Y μ)
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0

Tactic:
· simp [integral_sub (Integrable.of_mem_Icc a b hm hb) (integrable_const _)]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)
h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag
⊢ HasSubgaussianMGF ((fun p ↦ X p.1 + Y p.2) ∘ Function.diag) (cX + cY) μ

Tactic:
refine HasSubgaussianMGF.of_map ?_ this

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)
h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag
⊢ AEMeasurable Function.diag μ
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
exact✝ : S.Exact
mono_f : Mono S.f
epi_g : Epi S.g
⊢ (S.map (resFunctor φ)).Exact

Tactic:
by rwa [ShortComplex.exact_map_iff_of_faithful]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * ∑ g, W.character g * V.character g⁻¹ = ↑(finrank k (V ⟶ W))

Tactic:
conv_lhs => congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]
  -- The scalar product is the character of `Hom(V, W).`
  rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']

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
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = (IndV.mk S.subtype A.ρ g) (↑f g)

Tactic:
Finset.sum_eq_single ⟦g⟧

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = (IndV.mk S.subtype A.ρ g) (↑f g)

case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

case h₁
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧ ∉ Finset.univ → ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
x : ↑A
⊢ (((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ A.ρ g) x =
    ((MonoidHom.comp B.ρ φ) g ∘ₗ (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) x

Tactic:
have := (hom_comm_apply f (φ g) (IndV.mk φ A.ρ 1 x)).symm

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
x : ↑A
this : (B.ρ (φ g)) ((Hom.hom f) ((IndV.mk φ A.ρ 1) x)) = (Hom.hom f) (((ind φ A).ρ (φ g)) ((IndV.mk φ A.ρ 1) x))
⊢ (((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ A.ρ g) x =
    ((MonoidHom.comp B.ρ φ) g ∘ₗ (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) (η * ((galRestrict A K L B) g) a) = (algebraMap B L) a

Tactic:
rw [map_mul, ← hε]

Goal state after:
case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) g) a) = (algebraMap B L) η * ↑g ((algebraMap B L) a)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : x ∈ Coinvariants.ker A.ρ
y : ↑(ModuleCat.of k (G →₀ ↑A))
hy : (ModuleCat.Hom.hom (d₁₀ A)) y = x
⊢ ∃ a, (ConcreteCategory.hom (chains₁ToCoinvariantsKer A)) a = ⟨x, hx⟩

Tactic:
use y, Subtype.ext hy

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G →₀ ↑A
⊢ x ∈ cycles₁ A ↔ (x.sum fun g a ↦ (A.ρ g⁻¹) a) = x.sum fun x a ↦ a

Tactic:
change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G →₀ ↑A
⊢ (x.sum fun g a ↦ (A.ρ g⁻¹) a - a) = 0 ↔ (x.sum fun g a ↦ (A.ρ g⁻¹) a) = x.sum fun x a ↦ a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCycles A 2 ≫ (chainsIso₂ A).hom

Tactic:
by
  simp [isoCycles₂, iCycles, HomologicalComplex.iCycles, ShortComplex.iCycles]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
by
      suffices ∀ i : ℕ, ∃ j : ℕ, (↑(I ^ j) * ↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R) by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using! this
      intro n
      use n
      rintro a ⟨x, _hx, b, hb, rfl⟩
      exact (I ^ n).smul_mem x hb

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

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
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x ↦ x • m) ⁻¹' ↑(I ^ i • ⊤)

Tactic:
replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x ↦ x • m) ⁻¹' ↑(I ^ i • ⊤)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J

Tactic:
rintro ⟨H₁, H₂⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsAdic J
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
intro V

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
⊢ V ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
⊢ (toMvPowerSeries i) (C r) = MvPowerSeries.C r

Tactic:
toMvPowerSeries_apply,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
⊢ (MvPowerSeries.rename fun x ↦ i) (C r) = MvPowerSeries.C r
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (toMvPowerSeries i) X = MvPowerSeries.X i

Tactic:
toMvPowerSeries_apply,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (MvPowerSeries.rename fun x ↦ i) X = MvPowerSeries.X i
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
⊢ (toMvPowerSeries i) f = subst (MvPowerSeries.X i) f

Tactic:
toMvPowerSeries_apply,

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
⊢ (MvPowerSeries.rename fun x ↦ i) f = subst (MvPowerSeries.X i) f
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ (MvPowerSeries.coeff d) ((toMvPowerSeries i) f) = 0

Tactic:
toMvPowerSeries_apply,

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ (MvPowerSeries.coeff d) ((MvPowerSeries.rename fun x ↦ i) f) = 0
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
⊢ RingHom.ker (evalOneₐ I).toRingHom = Ideal.map (algebraMap R (AdicCompletion I R)) I

Tactic:
by
  ext x
  trans x ∈ (AdicCompletion.eval I R 1).ker
  · have eq : I ^ 1 * ⊤ = I := by simp
    have : Function.Injective (Ideal.Quotient.factor ((le_of_eq eq))) := by
      simpa [RingHom.injective_iff_ker_eq_bot, Ideal.Quotient.factor_ker]
        using Ideal.map_mk_eq_bot_of_le (le_of_eq eq.symm)
    simpa [← factorₐ_evalₐ_one, ← factor_eval_eq_evalₐ] using map_eq_zero_iff _ this
  · simp [← pow_smul_top_eq_ker_eval fg]

Goal state after:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
p : P
q : Q
⊢ 1 ⊗ₜ[R] (f p ⊗ₜ[R] g q) = (AlgebraTensorModule.assoc R R K K M N) ((1 • (algebraMap R K) 1 ⊗ₜ[R] f p) ⊗ₜ[R] g q)

Tactic:
simp only [map_one, one_smul, AlgebraTensorModule.assoc_tmul]

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
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹

Tactic:
change _ = ite _ _ _ * (ite _ _ _)⁻¹

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
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)))⁻¹
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case C
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
| C r =>

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
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (g m)
x✝¹ : ℕ
x✝ : M
⊢ f (dp R x✝¹ x✝) = (lift hI g hg) (dp R x✝¹ x✝)

Tactic:
by rw [lift_apply_dp, hf]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
by
  by_cases! hmn : m < n
  · exact dpow_add_of_lt hn_fac hmn hx hy
  · have h_sub : I ^ m ≤ I ^ n := Ideal.pow_le_pow_right hmn
    rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]
    simp only [dpow]
    have hxy : (x + y) ^ m = 0 := by
      rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
      exact Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)
    rw [hxy, mul_zero, eq_comm]
    apply Finset.sum_eq_zero
    intro k hk
    rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), mul_assoc, ← mul_assoc]
    apply mul_eq_zero_of_right
    rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
    apply Set.mem_of_subset_of_mem h_sub
    rw [← Finset.mem_antidiagonal.mp hk, add_comm, pow_add]
    exact Ideal.mul_mem_mul (Ideal.pow_mem_pow hy _) (Ideal.pow_mem_pow hx _)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
⊢ hI.IsSubDPIdeal (I ⊓ ⨅ i, J i)

Tactic:
cases isEmpty_or_nonempty ι with
  | inr _ =>
    refine ⟨fun _ hx ↦ hx.1, ?_⟩
    intro n hn x hx
    simp only [Ideal.mem_inf, mem_iInf] at hx ⊢
    exact ⟨hI.dpow_mem hn hx.1, fun i ↦  IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩
  | inl _ =>
    simp only [iInf_of_empty, le_top, inf_of_le_left]
    exact IsSubDPIdeal.self hI

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ ⊤ ≠ Ideal.ofList rs' • ⊤

Tactic:
refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ {r | r ∈ rs} = {r | r ∈ rs'}