mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ basicOpen f = ⊥ ↔ IsNilpotent f

Tactic:
rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ∈ comap ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) (stabilizer (↥(zmultiples a)) b)

Tactic:
mem_comap,

Goal state after:
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ∈ stabilizer (↥(zmultiples a)) b
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)

Tactic:
by simp [pow_add, pow_mul, pow_exponent_eq_one]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case pos
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
j : ι
h : i = j
⊢ (Pi.single i f * x) j = 0 j

Tactic:
subst h

Goal state after:
case pos
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x i = 0
⊢ (Pi.single i f * x) i = 0 i
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ zpowers g = ⊤

Tactic:
subst h

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
hg : g ≠ 1
hp : Fact (Nat.Prime (Nat.card G))
⊢ zpowers g = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ comap (Pi.evalRingHom R i) q ∈ comap (Pi.evalRingHom R i) '' ↑(basicOpen f)

Tactic:
exact ⟨q, by simpa using hp, by ext; simp⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a : ↑(Set.range f)
⊢ (IsLocalization.Away.awayToAwayRight ↑a ↑a) ((algE a) (x (e.symm a))) =
    (IsLocalization.Away.awayToAwayLeft ↑a ↑a) ((algE a) (x (e.symm a)))

pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ (IsLocalization.Away.awayToAwayRight ↑a ↑b) ((algE a) (x (e.symm a))) =
    (IsLocalization.Away.awayToAwayLeft ↑b ↑a) ((algE b) (x (e.symm b)))

Tactic:
· rfl

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ (IsLocalization.Away.awayToAwayRight ↑a ↑b) ((algE a) (x (e.symm a))) =
    (IsLocalization.Away.awayToAwayLeft ↑b ↑a) ((algE b) (x (e.symm b)))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k

Tactic:
orderOf_pow' t (pow_ne_zero k hp.ne_zero),

Goal state after:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t / (orderOf t).gcd (p ^ k) = orderOf t / p ^ k
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ↑(⟨ϕ ↑g, ⋯⟩ ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
H.coe_pow,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ↑⟨ϕ ↑g, ⋯⟩ ^ p ^ j = ↑1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
have : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← H.card_mul_index]
    exact mul_ne_zero h1 h2

Goal state after:
case neg
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
this : Finite G
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Group.FG ↥H
inst✝ : Group.FG ↥K
h : H = K
⊢ rank ↥H = rank ↥K

Tactic:
subst h

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ inst✝ : Group.FG ↥H
⊢ rank ↥H = rank ↥H
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect b.natDegree (C r) * reflect 1 X - reflect (b.natDegree + 1) 1) * eval r (reflect c.natDegree c) = 0

Tactic:
simp [← pow_succ']

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α

Tactic:
subst h

Goal state after:
α : Type u_1
inst✝ : Group α
hp : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
⊢ a * b = b * a

Tactic:
let ⟨m, hm⟩ := hx ⟨f a, a, rfl⟩

Goal state after:
G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
⊢ a * b = b * a
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
⊢ ¬p ∣ (↑P).index

Tactic:
by
  intro h
  rw [P.index_eq_card] at h
  obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card' (G := G ⧸ (P : Subgroup G)) p h
  have h := IsPGroup.of_card (((Nat.card_zpowers x).trans hx).trans (pow_one p).symm)
  let Q := (zpowers x).comap (QuotientGroup.mk' (P : Subgroup G))
  have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_isPGroup
    rw [QuotientGroup.ker_mk']
    exact P.2
  replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
  rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
    QuotientGroup.ker_mk'] at hp
  exact hp.ne' (P.3 hQ hp.le)

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Subsingleton (G ⧸ torsion G) ↔ IsMulTorsion G

Tactic:
QuotientGroup.subsingleton_iff,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ torsion G = ⊤ ↔ IsMulTorsion G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d

Tactic:
have h : (powMonoidHom d : G →* G).ker.index ≠ 0 := Subgroup.index_ne_zero_of_finite
  rw [← mul_left_inj' h, Subgroup.card_mul_index, index_powMonoidHom_ker, Nat.mul_div_cancel']
  exact Nat.gcd_dvd_left (Nat.card G) d

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun i

Tactic:
rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ i ≤ j ∨ j ≤ i
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m

Tactic:
have ⟨s, e, h⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M

Goal state after:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
e : M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m
h : sSupIndep s ∧ ∀ (m : ↑s), IsSimpleModule R ↥↑m
⊢ ∃ s x, ∀ (m : ↑s), IsSimpleModule R ↥↑m
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : n ∈ comap ((LinearMap.lsmul R M) r) (I • span R ∅)
hn : n ∈ N
⊢ r • n = 0

Tactic:
mem_comap,

Goal state after:
case empty
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set M
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : ((LinearMap.lsmul R M) r) n ∈ I • span R ∅
hn : n ∈ N
⊢ r • n = 0
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : i ∈ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s

Tactic:
mem_comap,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : ((LinearMap.lsmul R M) r) i ∈ I • (R ∙ i) ⊔ I • span R s
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : i = 0
⊢ 1 ∈ I ^ i

Tactic:
subst h

Goal state after:
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ 1 ∈ I ^ 0
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : i = 0
⊢ (algebraMap R R) r ∈ I ^ i

Tactic:
subst h

Goal state after:
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
⊢ (algebraMap R R) r ∈ I ^ 0
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
· apply Algebra.adjoin_le _
    rintro _ ⟨r, hr, rfl⟩
    exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])

Goal state after:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : n ∈ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
mem_comap,

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : ((LinearMap.lsmul R M) r) n ∈ I • (R ∙ i) ⊔ I • span R s
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S✝ : Type v
S' : Type w
inst✝¹⁴ : CommRing R
inst✝¹³ : CommSemiring S✝
inst✝¹² : Algebra S✝ R
inst✝¹¹ : CommSemiring S'
inst✝¹⁰ : Algebra S' R
inst✝⁹ : Algebra S✝ S'
inst✝⁸ : IsScalarTower S✝ S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
r : R
x : I.Cotangent
⊢ (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (r • x) =
    (RingHom.id R) r • (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun x

Tactic:
by
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    exact map_smul f _ _

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
J : Type u_4
inst✝ : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)

Tactic:
rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : S
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ideal R S

Tactic:
simp [RingHom.mem_ker]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom ⋯ b = eqToHom ⋯
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ φ₂ : X ⟶ Y
h : φ₁ = φ₂
⊢ mapMap φ₁ p = mapMap φ₂ p

Tactic:
subst h

Goal state after:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ : X ⟶ Y
⊢ mapMap φ₁ p = mapMap φ₁ p
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : i✝ = j
⊢ eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ = 𝟙 (if i✝ = j then A else 0)

Tactic:
subst h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
A : V
i✝ : ι
⊢ eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ = 𝟙 (if i✝ = i✝ then A else 0)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
h : i✝ = j
⊢ eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ = (eqToHom ⋯ ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ g ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
⊢ eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ = (eqToHom ⋯ ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ g ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

Tactic:
subst h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : (single V c i).obj A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

Tactic:
subst h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : K ⟶ (single V c i).obj A
hfg : f.f i = g.f i
⊢ f.f i = g.f i
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
⊢ (K.XIsoOfEq ⋯).inv ≫ K.d p₂ p₃ = K.d p₂ p₃
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq ⋯).hom = K.d p₁ p₂
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₃ p₁ : ι
⊢ K.d p₁ p₃ ≫ (K.XIsoOfEq ⋯).inv = K.d p₁ p₃
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
h : C₁ = C₂
n : ι
⊢ (eqToHom h).f n = eqToHom ⋯

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ : HomologicalComplex V c
n : ι
⊢ (eqToHom ⋯).f n = eqToHom ⋯
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'

Tactic:
subst h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n