mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
⊢ D (a ^ 0) = 0 • a ^ (0 - 1) • D a

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
⊢ D 1 = 0 • 1 • D a
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 : β
⊢ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ≤
    comap ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) (stabilizer (↥(zmultiples a)) b)

Tactic:
rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, natCast_zsmul]

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 : β
⊢ minimalPeriod (fun x ↦ a +ᵥ x) b • ⟨a, ⋯⟩ +ᵥ b = b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } ∈ (basicOpen f).carrier
⊢ r ∉ p.asIdeal.primeCompl

Tactic:
rw [h, Set.mem_singleton_iff] at this

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ p.asIdeal.primeCompl
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ (¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
push Not

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ orderOf 1 = p ^ 0

Tactic:
pow_zero,

Goal state after:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ orderOf 1 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : m = 0
⊢ False

Tactic:
hm0,

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * 0
hm0 : m = 0
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h₁ : f ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ 1 ∈ p.asIdeal

Tactic:
← add

Goal state after:
R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
h₁ : f ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ e + f ∈ p.asIdeal
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]

Tactic:
classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
  apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
  rwa [QuotientGroup.ker_mk']

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x ↦ exponent (M x)) ∣ exponent ((i : ι) → M i)

Tactic:
apply Finset.lcm_dvd fun i _ ↦ ?_

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
x✝ : i ∈ univ
⊢ exponent (M i) ∣ exponent ((i : ι) → M i)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (comap f '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑I)

Tactic:
· rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]
    exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑I)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: 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
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
⊢ 1 ∈ q.asIdeal

Tactic:
simpa [p] using! (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R ↦ ↑↑R) S
⊢ ∃ k, ⟨g, ⋯⟩ ^ p ^ k = 1

Tactic:
by
          refine Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)
          rwa [Subtype.ext_iff, coe_pow] at hk ⊢

Goal state after:
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 + (1 + c.natDegree)) (map (algebraMap R S) b * X ^ 0)) = 0

Tactic:
pow_zero,

Goal state after:
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 + (1 + c.natDegree)) (map (algebraMap R S) b * 1)) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
⊢ ∑ m ∈ d.divisors, #{a | orderOf a = m} = ∑ m ∈ d.divisors, φ m

Tactic:
sum_card_orderOf_eq_card_pow_eq_one hd0,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
⊢ #{x | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ rank G ≤ ∅.card

pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
⊢ Type ?u.15

Tactic:
exact rank_le (Subsingleton.elim _ _)

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : FG G
⊢ 0 < rank G

Tactic:
by
  rwa [pos_iff_ne_zero, ne_eq, rank_eq_zero_iff, not_subsingleton_iff_nontrivial]

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t

Tactic:
apply Subtype.coe_injective.injOn

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hα : Nontrivial α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Nat.card α)

Tactic:
replace hα : Nat.card α ≠ 1 := by contrapose! hα; exact (Nat.card_eq_one_iff_unique.mp hα).1

Goal state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : Nat.card α ≠ 1
⊢ Nat.Prime (Nat.card α)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case zero
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
hn : orderOf g = p ^ 0
⊢ g = 1

Tactic:
pow_zero,

Goal state after:
case zero
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
hn : orderOf g = 1
⊢ g = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
⊢ torsion G ≤ Subgroup.comap f (torsion H)

Tactic:
intro x
  exact f.isOfFinOrder

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
m : M
x✝ : m ∈ (AddCommGroup.torsion M).carrier
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun x ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun x ↦ r • m + x) n 0

Tactic:
{

Goal state after:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
m : M
x✝ : m ∈ (AddCommGroup.torsion M).carrier
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun x ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun x ↦ r • m + x) n 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
simp only [← Nat.card_eq_fintype_card]
    calc
      Nat.card (∀ p : ps, P p) = ∏ p : ps, Nat.card (P p) := Nat.card_pi
      _ = ∏ p : ps, p.1 ^ (Nat.card G).factorization p.1 := by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
      _ = ∏ p ∈ ps, p ^ (Nat.card G).factorization p :=
        (Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)
      _ = (Nat.card G).factorization.prod (· ^ ·) := rfl
      _ = Nat.card G := Nat.prod_factorization_pow_eq_self Nat.card_pos.ne'

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y a b : X
hm : IsMaximal x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ Iso (x, a) (b, y)

Tactic:
by subst a b; exact second_iso hm

Goal state after:
Module: Mathlib.Order.JordanHolder

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

Tactic:
rcases Set.mem_range.1 hy with ⟨j, rfl⟩

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
⊢ s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun 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
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Ideal.IsMaximal (toSpanSingleton R M m).ker

Tactic:
rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]
  exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

Goal state after:
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
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : ↥m ≃ₗ[R] N := (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
z : ↥m
eq : e z = g x
⊢ (f ∘ₗ m.subtype ∘ₗ ↑e.symm ∘ₗ g) x = g x

Tactic:
simp only [LinearMap.comp_apply, ← eq, LinearEquiv.coe_coe, e.symm_apply_apply]

Goal state after:
R : Type u_2
inst✝⁷ : Ring R
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
g : P →ₗ[R] N
m : Submodule R M
compl : IsCompl f.ker m
e : ↥m ≃ₗ[R] N := (f.ker.quotientEquivOfIsCompl m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
x : P
z : ↥m
eq : e z = g x
⊢ f (m.subtype z) = e z
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
M✝ : Type u_4
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
m : Submodule R M✝
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type u_7
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M × Submodule R M
h✝ : Iso X Y
e : Submodule R M × Submodule R M → Submodule R M × Submodule R M → Prop :=
  fun X Y ↦ Nonempty ((↥X.2 ⧸ Submodule.comap X.2.subtype X.1) ≃ₗ[R] ↥Y.2 ⧸ Submodule.comap Y.2.subtype Y.1)
x✝ y✝ : Submodule R M
h : IsMaximal x✝ (x✝ ⊔ y✝)
⊢ e (x✝, x✝ ⊔ y✝) (x✝ ⊓ y✝, y✝)

Tactic:
rw [sup_comm, inf_comm]; exact ⟨(LinearMap.quotientInfEquivSupQuotient ..).symm⟩

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)

Tactic:
mem_torsionBySet_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBy R M a ↔ torsionBySet R M {a} = ⊤

Tactic:
← isTorsionBySet_singleton_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBySet R M {a} ↔ torsionBySet R M {a} = ⊤
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
⊢ ↑(μ i) • x ∈ torsionBySet R M ↑(p i)

Tactic:
mem_torsionBySet_iff

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (↑S).Pairwise fun i j ↦ Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤

Tactic:
· congr
    ext : 1
    congr
    ext : 1
    exact (torsionBySet_span_singleton_eq _).symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (↑S).Pairwise fun i j ↦ Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : ↥R⁰
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • x✝¹ = 0

Tactic:
← hb,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : ↥R⁰
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • b • x = 0
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
⊢ I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal

Tactic:
refine
  { LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare
      fun x => by rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _,
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
  · rintro x y e
    replace e := congr_arg Subtype.val e
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    obtain ⟨y, rfl⟩ := I.toCotangent_surjective y
    rw [I.toCotangent_eq]
    dsimp only [toCotangent_to_quotient_square, Submodule.mkQ_apply] at e
    rwa [Submodule.Quotient.eq] at e
  · rintro ⟨_, x, hx, rfl⟩
    exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩

Tactic:
simp [I.cotangentEquivIdeal.symm_apply_eq, Subtype.ext_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.span R s = ⊤

Tactic:
← Submodule.restrictScalars_span R (ResidueField R)
        Ideal.Quotient.mk_surjective,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.restrictScalars R (Submodule.span (ResidueField R) s) = ⊤
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
xeq : x = J.toCotangent ⟨z, zmemJ⟩
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
rw [xeq]

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
xeq : x = J.toCotangent ⟨z, zmemJ⟩
⊢ J.toCotangent ⟨z, zmemJ⟩ ∈
    Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))