mathlib-initiative/mathlib-tactics huggingface dataset:
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
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ (resFunctor φ).obj Y✝
⊢ (indResHomEquiv φ X'✝ Y✝).toEquiv.symm (x✝¹ ≫ x✝) =
    (indFunctor k φ).map x✝¹ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝

Tactic:
change (indResHomEquiv φ _ _).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
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ (resFunctor φ).obj Y✝
⊢ (indResHomEquiv φ X'✝ Y✝).symm (x✝¹ ≫ x✝) = (indFunctor k φ).map x✝¹ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝
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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
g : G
⊢ TensorProduct.lift
        (((lift (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) k
              H)
            fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g =
    TensorProduct.lift
      (((lift (↑A →ₗ[k] ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants) k H)
          fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
        ↑(MonoidAlgebra.coeffLinearEquiv k))

Tactic:
ext; simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff]
        using! Coinvariants.sub_mem_ker _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ QuasiIso (εToSingle₀ k G)

Tactic:
← HomologicalComplex.quasiIso_map_iff_of_preservesHomology _ (forget₂ _ (ModuleCat.{u} k))

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0
⊢ span (m.leadingTerm '' B) = span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

Tactic:
rw [← m.span_leadingTerm_sdiff_singleton_zero]
  apply span_leadingTerm_eq_span_monomial
  simp_intro .. [or_iff_not_imp_right.mp (hB _ _)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
  intro f hf
  rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]
  exact sub_mem hf (I.mul_mem_right _ hXI)

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

Goal state before:
pp: case mem
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
hz : z ∈ {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

Tactic:
rcases hz with h | h

Goal state after:
case mem.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∃ x ∈ span T, constantCoeff x = constantCoeff f

Tactic:
refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
s : R
hs : s ∈ S
⊢ ∃ x ∈ span T, constantCoeff x = s

case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (x y : R),
    x ∈ Submodule.span R S →
      y ∈ Submodule.span R S →
        (∃ x_1 ∈ span T, constantCoeff x_1 = x) →
          (∃ x ∈ span T, constantCoeff x = y) → ∃ x_1 ∈ span T, constantCoeff x_1 = x + y

case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (a x : R),
    x ∈ Submodule.span R S → (∃ x_1 ∈ span T, constantCoeff x_1 = x) → ∃ x_1 ∈ span T, constantCoeff x_1 = a • x
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 : ℕ
A B : Rep k G
f : A ⟶ B
inst✝ : Epi f
Z✝ : ModuleCat k
g h : groupHomology B 0 ⟶ Z✝
hgh : map (MonoidHom.id G) f 0 ≫ g = map (MonoidHom.id G) f 0 ≫ h
⊢ g = h

Tactic:
simp only [← cancel_epi (H0π A)] at hgh
    simp_all [cancel_epi]

Goal state after:
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 S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1 = 0

Tactic:
rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]

Goal state after:
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 S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S) 1 = 0

Tactic:
rw [← map_comp, congr (QuotientGroup.mk'_comp_subtype S) (map (n := 1)), map₁_one]

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

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

Tactic:
by_cases h : r = 0 <;>
  simp [h, Set.singleton_zero, contentIdeal_def, coeffs_monomial]

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

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi : (algebraMap R K) v' * (algebraMap R K) i' = 1
iv : (algebraMap R K) i' * (algebraMap R K) v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv, inv_val := vi } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v' i' : R
vi✝ : (algebraMap R K) v' * (algebraMap R K) i' = 1
vi : v' * i' = 1
iv : (algebraMap R K) i' * (algebraMap R K) v' = 1
hx :
  (powMonoidHom n) { val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := (algebraMap R K) v', inv := (algebraMap R K) i', val_inv := vi✝, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := (algebraMap R K) i', inv := (algebraMap R K) v', val_inv := iv, inv_val := vi✝ } ^ n =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0

pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : ¬m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0

Tactic:
· simp [hm, uniformBell_zero_left, hn]

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : ¬m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ dp R n m ^ k = ↑(k • {n}).multinomial * dp R (k * n) m

Tactic:
Multiset.multinomial_nsmul_singleton,

Goal state after:
R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ dp R n m ^ k = ↑(Nat.multinomial (range k) fun x ↦ n) * dp R (k * n) m
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = (insert a s).erase a

Tactic:
erase_insert ha

Goal state after:
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = s
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✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r • ⊤ = ⊤

Tactic:
exact Eq.trans (Submodule.map_top _) <| LinearMap.range_eq_top.mpr <|
      surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left

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

Goal state before:
pp: case cons
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs✝ : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
r : R
rs : List R
h₄ : IsSMulRegular M✝ r
h2✝ : IsWeaklyRegular (QuotSMulTop r M✝) rs
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
ih :
  Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₂) ⋯)
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
H₁ :
  ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ
      (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯ =
    (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯ ∘ₗ
      ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)
⊢ Exact ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯)

Tactic:
have H₂ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₂

Goal state after:
case cons
R : Type u_1
M₄ : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M₄
inst✝⁸ : Module R M₄
rs✝ : List R
M✝ : Type u_6
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
r : R
rs : List R
h₄ : IsSMulRegular M✝ r
h2✝ : IsWeaklyRegular (QuotSMulTop r M✝) rs
M : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f₁ : M →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
ih :
  Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯)
    ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₂) ⋯)
f₃ : M₃ →ₗ[R] M✝
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h₃ : Surjective ⇑f₃
H₁ :
  ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ
      (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯ =
    (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₁) ⋯ ∘ₗ
      ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)
H₂ :
  ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₃ r rs) ∘ₗ
      (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯ =
    (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f₂) ⋯ ∘ₗ
      ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs)
⊢ Exact ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₁ ⋯)
    ⇑((Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f₂ ⋯)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.IsSubDPIdeal (J ⊓ I)

Tactic:
refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
    rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
    exact hIJ ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x

Tactic:
nth_rewrite 1 [← one_smul R (hI.dpow n x)]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : (fun s ↦ ↑s.carrier) p = (fun s ↦ ↑s.carrier) q
⊢ p = q

Tactic:
SetLike.coe_set_eq

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
p q : hI.SubDPIdeal
h : p.carrier = q.carrier
⊢ p = q
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr
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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
obtain ⟨U, _, _, ⟨e⟩⟩ := Algebra.FormallyUnramified.exists_algEquiv_prod R S

Goal state after:
case succ.inr
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
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : WeaklyEtale R S
⊢ (TensorProduct.lmul' T).Flat

Tactic:
let e : T ⊗[R] S ⊗[T] (T ⊗[R] S) ≃ₐ[T] T ⊗[R] (S ⊗[R] S) :=
      (Algebra.TensorProduct.cancelBaseChange _ _ T _ _).trans
        (TensorProduct.assoc ..)
    have : TensorProduct.lmul' T (S := T ⊗[R] S) =
        (TensorProduct.map (.id T T) (TensorProduct.lmul' R)).comp e.toAlgHom := by
      ext <;> simp [e, TensorProduct.one_def]
    rw [this]
    refine .comp (.of_bijective e.bijective) (.tensorProductMap ?_ ?_)
    · exact .of_bijective Function.bijective_id
    · exact WeaklyEtale.flat_lmul' R S

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x✝ : ℕ
ih : ⇑(f ^ x✝) = (⇑f)^[x✝]
⊢ ⇑(f ^ x✝.succ) = (⇑f)^[x✝.succ]

Tactic:
ext; simp [pow_succ, ih]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (subst ![X₁, X₀] F.toPowerSeries) = subst ![g, f] F.toPowerSeries

Tactic:
subst_comp_subst_apply HasSubst.X_X <| hasSubst_of_constantCoeff_nilpotent (by simp [hf, hg])

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst (fun s ↦ subst ![f, g] (![X 1, X 0] s)) F.toPowerSeries = subst ![g, f] F.toPowerSeries
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ g ∈ ⋃ a, (s (e.symm a)).support → g ∈ ⋃ a, (s a).support

Tactic:
simp only [Set.mem_iUnion, mem_support, ne_eq, forall_exists_index]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∀ (x : β), ¬(s (e.symm x)).coeff g = 0 → ∃ i, ¬(s i).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
⊢ (⋃ a, (f a • s a).support).IsPWO

Tactic:
refine Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
hg : g ∈ ⋃ a, (f a • s a).support
⊢ g ∈ ⋃ a, (s a).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
⊢ (a✝ ∈ Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) → a✝ ∈ ↑⋯.toFinset

Tactic:
hab

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : PartialOrder Γ
inst✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
hab : a✝ ∈ Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2
⊢ a✝ ∈ ↑⋯.toFinset
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ ∀ b ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}, maximalIdeal R ≤ b

Tactic:
rintro I ⟨-, hI⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
I : Ideal R
hI : I.IsMaximal
⊢ maximalIdeal R ≤ I
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
hpn : p ≠ ⊥
x : R
hxmem : x ∈ p
hxp : Prime x
⊢ Submodule.IsPrincipal p

Tactic:
exact ⟨x, p.eq_span_singleton_of_height_eq_one hph hxmem hxp⟩

Goal state after:
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp.mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ ↑(F • F)
⊢ I ∈ ↑F

Tactic:
rcases hI with ⟨J, hJ, htors⟩
      refine hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩
      rcases htors x hx with ⟨K, hK, hincl⟩
      exact Order.PFilter.mem_of_le hincl hK

Goal state after: