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

Goal state before:
pp: case hg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (A.indicator fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) P

Tactic:
· exact hg.indicator₀ mA

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 κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ ‖rexp (t * X ω)‖ₑ ^ ↑p = ‖rexp (↑p * t * X ω)‖ₑ

Tactic:
rw [enorm_eq_ofReal (by positivity), enorm_eq_ofReal (by positivity),
      ENNReal.ofReal_rpow_of_nonneg (by positivity), ← exp_mul, mul_comm, ← mul_assoc]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ ↑p
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
by
    have h'' := Measure.ae_ae_of_ae_comp h'
    filter_upwards [h.mgf_le, h''] with ω' h_mgf h' t
    rw [mgf_congr (Filter.EventuallyEq.symm h')]
    exact h_mgf t

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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0✝ : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
ω : Ω
hY0 : Y ω = 0 ω
⊢ X ω = X ω + Y ω

Tactic:
simp [hY0]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : ConditionallyCompleteLinearOrderBot ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ ⨅ j, ⨅ (_ : j ≥ x), τ j ω) atTop (𝓝 ⊤)

Tactic:
by
    filter_upwards [hτ.tendsto_top] with ω hω
    replace hω := hω.liminf_eq
    rw [liminf_eq_iSup_iInf_of_nat] at hω
    rw [← hω]
    refine tendsto_atTop_iSup fun n m hnm ↦ ?_
    simp [iInf_le_iff]
    grind

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case hs
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∀ᵐ (ω : Ω) ∂P, Antitone fun x ↦ ω ∈ {ω | σ n x ω < min (τ n ω) ↑(T n)}

Tactic:
filter_upwards [(hσ n).mono] with ω hω
    intros i j hij
    specialize hω hij
    simp [Set.ofPred] at *
    grind

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (fun x ↦ Y n x ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ

Tactic:
moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (y : ℝ) in 0..↑n, y ^ 2 ∂Measure.map X ℙ = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (Y j ^ 2) a = ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ

Tactic:
by simp_rw [Y2]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hbc
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ ∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹ ≤ 2 / (↑k + 1)

Tactic:
· apply sum_Ioo_inv_sq_le

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case succ
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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : V
hx : (ρ g) x = x
i : ℕ
a✝ : (ρ ((fun x ↦ g ^ x) ↑i)) x = x
⊢ (ρ ((fun x ↦ g ^ x) (↑i + 1))) x = x

Tactic:
simp_all [zpow_add_one]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ∀ (g : G), σ g ∘ₗ f ∘ₗ ρ g⁻¹ = f
γ : G
v : V
⊢ f ((ρ γ) v) = (σ γ) (f v)

pp: case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
⊢ σ γ ∘ₗ f ∘ₗ ρ γ⁻¹ = f

Tactic:
· specialize hf γ
    nth_rewrite 1 [← hf]
    simp

Goal state after:
case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
⊢ σ γ ∘ₗ f ∘ₗ ρ γ⁻¹ = f
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V W : FDRep k G
g : G
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g

Tactic:
← char_iso (dualTensorIsoLinHom _ _),

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V W : FDRep k G
g : G
⊢ (of (dual V.ρ) ⊗ W).character g = V.character g⁻¹ * W.character g
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
let Y : ℕ → Ω → ℝ := fun n ↦ F ∘ (X n)

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero, tendsto_order]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < a'
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
h :
  (shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ⇑x ∈ coboundaries₁ A

Tactic:
simp only [H1π, isoCocycles₁, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
h :
  (shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom
⊢ (ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π) x = 0 ↔ ⇑x ∈ coboundaries₁ A
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ H2π A ≫ map f φ 2 = mapCocycles₂ f φ ≫ H2π B

Tactic:
by
  simp [H2π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₂_hom_assoc]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ ∅, J ≤ P

pp: case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
· exact ⟨⊥, by simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]⟩

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) C
w✝ : Ideal R
hI : w✝ ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
⊢ False

Tactic:
have hT₃ : T ≠ ⊥ := fun h₂ ↦ ha (span_singleton_eq_bot.1 ((h₂ ▸ hT₂) _ h zero_le))

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False

Tactic:
rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem] at hT

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
h : span {a} ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ kaplanskySet (closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
Tpri : T.IsPrime
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case refine_3
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
x : σ →₀ ℕ
hx : x ∈ Set.Finite.toFinset ⋯
⊢ (coeff x) p • (coeff n) (x.prod fun s e ↦ (X ∘ f) s ^ e) = (coeff x) p

Tactic:
· simp only [Set.Finite.mem_toFinset] at hx
    simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n✝ : ℕ
F : Fin n✝ → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
n : ℕ
IH : g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
⊢ g - ∑ i, ↑((trunc (n + 1)) (H i)) * F i = X ^ (n + 1) * G (n + 1)

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ (finSuccEquiv R n) (X j.succ) = PowerSeries.C (X j)

Tactic:
ext k x
  simp_rw [coeff_coeff_finSuccEquiv, PowerSeries.coeff_C, coeff_X, cons_eq_single_succ_iff]
  split_ifs with h1 h2 h3
  · simp [h1.left]
  · tauto
  · rw [coeff_X, if_neg (by tauto)]
  · rw [coeff_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
⊢ Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R)))

Tactic:
refine ⟨RingHom.injective _, fun x ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
⊢ ∃ a, (IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R))) a = x
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ I.IsCoideal ↔ (∀ x ∈ I, counit x = 0) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range

Tactic:
simp_rw [isCoideal_iff, ← LinearMap.mem_ker,
    TensorProduct.map_ker (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective
      (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MulOpposite

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (map (↑(opLinearEquiv R)) (counit ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
      (comul (↑(opLinearEquiv R).symm x✝)) =
    ((TensorProduct.mk R Aᵐᵒᵖ R).flip 1) x✝

Tactic:
simp [← rTensor_comp_lTensor]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r).contentIdeal = span {r}

Tactic:
by
  rw [← monomial_zero_left]
  exact contentIdeal_monomial 0 r

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} → C r ∣ p

Tactic:
rw [← p.contentIdeal.span_singleton_generator]
    intro _
    calc
    C r ∣ C h_prin.generator := by
      apply _root_.map_dvd C
      rwa [← span_singleton_le_span_singleton]
     _ ∣ p := h_prin.contentIdeal_generator_dvd

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: 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

Tactic:
rw [hPprime.mul_le]

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 ≤ P ∨ q.contentIdeal ≤ P
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ mapDomainOfBialgHomFun f (g₁ * g₂) = mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂

Tactic:
refine single_left_injective (R := R) one_ne_zero ?_

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ (fun m ↦ single m 1) (mapDomainOfBialgHomFun f (g₁ * g₂)) =
    (fun m ↦ single m 1) (mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
g : G
⊢ (mapDomainOfBialgHom (mapDomainBialgHom R f)) g = f g

Tactic:
refine single_left_injective (R := R) one_ne_zero ?_

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
g : G
⊢ (fun m ↦ single m 1) ((mapDomainOfBialgHom (mapDomainBialgHom R f)) g) = (fun m ↦ single m 1) (f g)
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
isSMulRegular_on_quot_iff_lsmul_comap_le,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ comap ((LinearMap.lsmul R M) r) N ≤ N ↔ r • ⊤ ⊓ N ≤ r • N