mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ ↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g =
    (linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)

Tactic:
ext; simp [linearize_single _]; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
x : (leftRegular k G).IntertwiningMap σ
⊢ (fun v ↦
        { toLinearMap := ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
          isIntertwining' := ⋯ })
      ((fun f ↦ (Finsupp.llift V k k G).symm (f.toLinearMap ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k).symm) 1) x) =
    x

Tactic:
ext; simp [← x.isIntertwining]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.inl
Ω : 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 : ℕ
a✝ : 0 ∈ range (u (N - 1))
⊢ (∑ i ∈ range N with 0 < u i, (↑(u i) ^ 2)⁻¹) * Var[Y 0; ℙ] ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑0 ^ 2 * Var[Y 0; ℙ]

Tactic:
simp only [Nat.cast_zero]
          simp only [Y, Nat.cast_zero, truncation_zero, variance_zero, mul_zero, le_rfl]

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✝
G : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : FiniteDimensional k V
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
v' : Module.Dual k V
w : W
v : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(dualTensorHomEquiv k V W) ∘ₗ (ρ.dual.tprod σ) g)) v') w) v =
    (((TensorProduct.AlgebraTensorModule.curry ((ρ.linHom σ) g ∘ₗ ↑(dualTensorHomEquiv k V W))) v') w) v

Tactic:
simp [Module.Dual.transpose_apply]

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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
convert! hω.sub (h'ω.comp_tendsto A) using 1

Goal state after:
case e'_7
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ x⌋₊ * ∫ (a : Ω), X 0 a) -
      ((fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) ∘ fun n ↦ ⌊c ^ n⌋₊) x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ x ∈ cocycles₁ X.X₁

Tactic:
apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
  have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH1, LinearMap.compLeft]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ (ConcreteCategory.hom (δ hX 1 2 ⋯)) ((ConcreteCategory.hom (H1π X.X₃)) z) = (ConcreteCategory.hom (H2π X.X₁)) ⟨x, ⋯⟩

Tactic:
by
  simpa [H1π, H2π, ← cocyclesMk₂_eq X.X₁, ← cocyclesMk₁_eq X.X₃] using!
    δ_apply hX rfl ((cochainsIso₁ X.X₃).inv z) (by
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simp [cocycles₁.d₁₂_apply z]) ((cochainsIso₁ X.X₂).inv y) (by ext; simp [cochainsIso₁, ← hy])
    ((cochainsIso₂ X.X₁).inv x) <| by
      ext g
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simpa [← hx] using! congr_fun (congr($((CommSq.vert_inv
        ⟨cochainsMap_f_2_comp_cochainsIso₂ (MonoidHom.id G) X.f⟩).w) x)) g

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0

Tactic:
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
  rw [Set.image_image] at this
  refine this.trans ?_
  simp [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ ¬{t} ⊆ Set.range ⇑e

Tactic:
Set.singleton_subset_iff

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ t ∉ Set.range ⇑e
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔
    mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single g.2 a + single g.1 (g.1 • a)) =
      mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single (g.1 * g.2) (g.1 • a))

Tactic:
simp [mapRange_add, IsCycle₂]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this : WithIdeal R := { i := I }
⊢ IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R

Tactic:
let : WithIdeal S := ⟨I.map e⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this : WithIdeal R := { i := I }
⊢ IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R

Tactic:
let : WithIdeal S := ⟨I.map e⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1)

Tactic:
← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ (degree x + 1)),

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1) * ⊤
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : n ≤ i
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
k : ℕ
h : n ≤ k + n
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) (k + n) = ↑x (k + n)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ map ((QuotientGroup.mk' S).comp S.subtype)
      (𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.resOfQuotientIso S).inv) 1 =
    0

Tactic:
congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)),

Goal state after:
k G H : Type u
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ map 1 (⋯ ▸ 𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.resOfQuotientIso S).inv) 1 = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := ⋯
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := ⋯
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := ⋯
he : Function.Injective e
ve : G × G →₀ ↑A := ⋯
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f)
      ((ConcreteCategory.hom (H1π (res S.subtype A)))
        ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w⟩) =
    (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩

Tactic:
simp only [H1CoresCoinfOfTrivial_f, H1CoresCoinfOfTrivial_X₁, H1π_comp_map_apply]

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
hS : ↑(v + (ConcreteCategory.hom (d₂₁ A)) ve).support ⊆ ↑S
⊢ (ConcreteCategory.hom (H1π A))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype A))))
        ⟨comapDomain Subtype.val (v + (ConcreteCategory.hom (d₂₁ A)) ve) ⋯, ?w⟩) =
    (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
⊢ map ((QuotientGroup.mk' S).comp S.subtype) (𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.toCoinvariantsMkQ S))
      1 =
    0

Tactic:
congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)),

Goal state after:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
⊢ map 1 (⋯ ▸ 𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.toCoinvariantsMkQ S)) 1 = 0
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ᵐᵒᵖ
⊢ (↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) ∘ₗ rTensor Aᵐᵒᵖ comul ∘ₗ comul) x✝ = (lTensor Aᵐᵒᵖ comul ∘ₗ comul) x✝

Tactic:
rw [comul_def, rTensor_comp, rTensor_comp]
    simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_map, rTensor_def]
    simp_rw [← map_map_assoc, map_map, comp_assoc, ← lTensor_comp_rTensor]
    simp [lTensor_tensor, comp_assoc]

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

Goal state before:
pp: 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
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ∃ p ∈ associatedPrimes R M, annihilator R N ≤ p

Tactic:
apply (Ideal.subset_union_prime_finite (associatedPrimes.finite R M) Ia Ia _).mp

Goal state after:
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
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ↑(annihilator R N) ⊆ ⋃ i ∈ associatedPrimes R M, ↑i

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
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ∀ i ∈ associatedPrimes R M, i ≠ Ia → i ≠ Ia → i.IsPrime
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y = ∑ k ∈ antidiagonal n, hJ.dpow k.1 x * hJ.dpow k.2 y

Tactic:
apply sum_congr rfl

Goal state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∀ x_1 ∈ antidiagonal n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
⊢ r • x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
refine ⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f (hI.dpow n (r • x)) = hJ.dpow n (f (r • x))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ S
⊢ y ∈ { carrier := {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}, add_mem' := ⋯, zero_mem' := ⋯ }

Tactic:
exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩

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

Goal state before:
pp: case nil
R : Type u_1
inst✝² : CommRing R
rs₂ : List R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsWeaklyRegular M ([] ++ rs₂) ↔ IsWeaklyRegular M [] ∧ IsWeaklyRegular (M ⧸ Ideal.ofList [] • ⊤) rs₂

Tactic:
refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
    refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
    rw [Ideal.ofList_nil, bot_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊥ = ⊤
⊢ False

Tactic:
subsingleton_iff_bot_eq_top

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : Subsingleton (Submodule R M)
⊢ False
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Subsingleton R
this : Subsingleton S
⊢ IsFiniteSplit R S

Tactic:
exact of_subsingleton_top

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Subsingleton S
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
exact of_subsingleton_top

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr.refine_4
n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
⊢ IsFiniteSplit V (V ⊗[R] S)

Tactic:
· exact .of_algEquiv e.symm

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (h1Cotangentι ∘ₗ map (defaultHom R S P)).range = Submodule.map h1Cotangentι ⊤

Tactic:
← P.h1CotangentEquivCotangent_comp_map,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S).range = Submodule.map h1Cotangentι ⊤
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ f (hI.dpow n a) = hK'.dpow n (f a)

Tactic:
hIK'.2 a ha

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ ↑I
n : ℕ
⊢ f (hI.dpow n a) = f (hI.dpow n a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
⊢ dpow hI f 0 x = 1

Tactic:
by
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]

Goal state after: