mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁷ : Semiring 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
f : ρ.IntertwiningMap σ
g : G
w : W
x✝ : w ∈ f.range
v : V
hv : f.toLinearMap v = w
⊢ f.toLinearMap ((ρ g) v) = (σ g) w

Tactic:
by
    simp [f.isIntertwining, (f.toLinearMap_apply _ _ _).symm.trans hv]

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✝¹³ : Semiring 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✝
V : Type u_6
W : Type u_7
P : Type u_8
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup P
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f✝ : V →ₗ[A] W
f g : ρ.IntertwiningMap σ
⊢ ∀ (g_1 : G), (f.toLinearMap - g.toLinearMap) ∘ₗ ρ g_1 = σ g_1 ∘ₗ (f.toLinearMap - g.toLinearMap)

Tactic:
by
    simp [LinearMap.sub_comp, LinearMap.comp_sub, f.2, g.2]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
N : ℕ
⊢ c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤
    c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)

Tactic:
apply mul_le_mul_of_nonneg_left (I1 _)

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
N : ℕ
⊢ 0 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G✝ : Type v
inst✝³ : CommRing R
inst✝² : Field k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Monoid G
⊢ LargeCategory (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ ConcreteCategory (FDRep R G) (Action.HomSubtype (FGModuleCat R) G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Preadditive (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasFiniteLimits (FDRep k G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Linear R (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
V : FDRep R G
⊢ Module.Finite R ↑V.V

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalCategory (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalPreadditive (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalLinear R (FDRep R G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasKernels (FDRep k G)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ ((ModuleCat.isFG R).ι.mapAction G ⋙ Rep.ActionToRep R G).Full

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ ((ModuleCat.isFG R).ι.mapAction G ⋙ Rep.ActionToRep R G).Faithful

Tactic:
infer_instance

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat k[G]
⊢ (Representation.ofModule ↑M).asModule ≃+ ↑M

Tactic:
exact (Representation.ofModule M).asModuleEquiv.toAddEquiv.trans
    (RestrictScalars.addEquiv k k[G] _)

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: 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
a✝ b✝ : V
hv : a✝ ∈ {v | ∀ (g : G), (ρ g) v = v}
hw : b✝ ∈ {v | ∀ (g : G), (ρ g) v = v}
g : G
⊢ (ρ g) (a✝ + b✝) = a✝ + b✝

Tactic:
simp only [hv g, hw g, map_add]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
⊢ (sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • (sumOfConjugates G π) v

Tactic:
by
    simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
    refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
    simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
x✝² x✝¹ : π₁ →ⁱL π₂
x✝ : (fun f ↦ f.toIntertwiningMap) x✝² = (fun f ↦ f.toIntertwiningMap) x✝¹
⊢ x✝² = x✝¹

Tactic:
ext; simp_all

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
i : (forget (Rep k G)).obj X ≅ (forget (Rep k G)).obj Y := asIso ((forget (Rep k G)).map f)
e : X.ρ.Equiv Y.ρ :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toIntertwiningMap := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
exact (mkIso e).isIso_hom

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

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
⊢ ?m.292

Tactic:
by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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.ρ ⟨↑s * s₁ • g * g⁻¹, ⋯⟩) a =
    (A.ρ s) ((if h : (QuotientGroup.rightRel S) (s₁ • g) g then A.ρ ⟨s₁ • g * g⁻¹, ⋯⟩ else 0) a)

Tactic:
dif_pos ⟨s₁, rfl⟩

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.ρ ⟨↑s * s₁ • g * g⁻¹, ⋯⟩) a = (A.ρ s) ((A.ρ ⟨s₁ • g * g⁻¹, ⋯⟩) a)
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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ : G
a : ↑A
s : ↥S
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) ((fun m ↦ m • g₁) s) = (Hom.hom f) ((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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (Y.resolutionX i).ρ.coind₁.coind₁ι.comp (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))

Tactic:
← coind₁ResMap_comp_coind₁ι_restrict

Goal state after:
case succ
k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih :
  (Hom.hom (Y.d i)).comp (Hom.hom (resolutionMap φ f i)) =
    (coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))
⊢ (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i)))) =
    (coind₁ResMap φ (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))).comp
        (ContIntertwiningMap.restrict (↑φ) (X.resolutionX i).ρ.coind₁.coind₁ι) -
      coind₁ResMap φ
        ((coind₁ResMap φ (Hom.hom (resolutionMap φ f i))).comp (ContIntertwiningMap.restrict (↑φ) (Hom.hom (X.d i))))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: 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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
have hxinv : Algebra.norm K x⁻¹ = 1 := by simp [Algebra.norm_inv, hx]

Goal state after:
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)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
⊢ ∃ y, ↑y / g ↑y = 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ˣ := 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 (IsLocalization.mk' L a b) = IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
replace hε := congr_arg (t • ·) 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ε : t • ((algebraMap B L) η * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = 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
⊢ (cochainsIso₂ A).hom ≫ d₂₃ A = (inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom

Tactic:
ext x y
  change A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
  dsimp
  rw [Fin.sum_univ_three]
  simp only [sub_eq_add_neg, add_assoc, Fin.val_zero, zero_add, pow_one, neg_smul,
    one_smul, Fin.val_one, Fin.val_two, pow_succ' (-1 : k) 2, neg_sq, Nat.one_add, one_pow, mul_one]
  rcongr i <;> fin_cases i <;> rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (g : G),
    (rightFDRep ⊗ rightFDRep).ρ g ≫ InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) =
      InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) ≫ rightFDRep.ρ g

Tactic:
intro

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
g✝ : G
⊢ (rightFDRep ⊗ rightFDRep).ρ g✝ ≫ InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) =
    InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) ≫ rightFDRep.ρ g✝
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
⊢ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} ⊆
    ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))

Tactic:
intro

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
a✝ : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝ ∈ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} →
    a✝ ∈ ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} ⊆
    ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))

Tactic:
intro

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
a✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝ ∈ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} →
    a✝ ∈ ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
b : R
hx₂ : b * a ∈ ↑(closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
b : R
hx₂ : a * b ∈ ↑(closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R

Tactic:
refine UniqueFactorizationMonoid.of_exists_prime_factors fun a ha ↦ ?_
  have ha₂ := span_notMem_kaplanskySet ha H
  rw [mem_kaplanskySet_iff] at ha₂
  rcases nonempty_iff_ne_empty.2 ha₂ with ⟨x, hx, hx₂⟩
  obtain ⟨b, hb⟩ := mem_span_singleton'.1 hx
  rw [← hb, mul_comm] at hx₂
  have hsubset : closure {r : R | Prime r} ≤ closure {r : R | IsUnit r ∨ Prime r} :=
    closure_mono (by grind)
  have := divisor_closure_eq_closure _ _ (hsubset hx₂)
  clear ha ha₂ hx hb hx₂
  induction this using closure_induction with
  | mem z hz =>
      rcases hz with h | h
      · exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩
      · exact ⟨{z}, by simpa⟩
  | one => exact ⟨∅, by simp⟩
  | mul z₁ z₂ hz₁ hz₂ h₁ h₂ =>
      obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
⊢ ∃ x ∈ P, Prime x

Tactic:
by_cases hXP : X ∈ P

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∈ P
⊢ ∃ x ∈ P, Prime x

case neg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ NonarchimedeanRing R

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ IsTopologicalRing (UniformSpace.Completion R)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsTopologicalAddGroup M

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ContinuousSMul R M

Tactic:
infer_instance

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
n : ℕ
⊢ p - (truncTotal n) ↑p ∈ MvPolynomial.idealOfVars σ R ^ n

Tactic:
exact (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr fun x hx ↦ by simp [coeff_truncTotal _ hx]

Goal state after: