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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ D (a ^ ↑n.natAbs)⁻¹ = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a

Tactic:
zpow_natCast,

Goal state after:
case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ D (a ^ n.natAbs)⁻¹ = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1

Tactic:
simp_rw [← pow_eq_mod_exponent]

Goal state after:
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ IsOpenMap (sigmaToPi R)

Tactic:
rw [isOpenMap_sigma]
    intro i
    simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
    rintro - ⟨f, rfl⟩
    rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
    exact isOpen_basicOpen

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

Goal state before:
pp: case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ ↑(m / (Fintype.card α / n.gcd (Fintype.card α))) = x

Tactic:
zpow_natCast,

Goal state after:
case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ (g ^ (Fintype.card α / n.gcd (Fintype.card α))) ^ (m / (Fintype.card α / n.gcd (Fintype.card α))) = x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p

pp: case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p

pp: case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G

Tactic:
· rw [Ne, ← orderOf_eq_one_iff] at hg
    exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ exponent G ∣ p

case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ g ^ exponent ↥S = 1

Tactic:
by
  have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
  rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

Goal state after:
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
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ 1 = (orderOf (t ^ p ^ k)).factorization p + 1

Tactic:
rw [hpk', Nat.factorization_div hpk]

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
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ 1 = ((orderOf t).factorization - (p ^ k).factorization) p + 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
⊢ ∃ g, orderOf g = exponent G

Tactic:
have he := hG.exponent_ne_zero
  have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
  have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
    rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
  obtain ⟨t, ht⟩ := hne.csSup_mem hfin
  use t
  apply Nat.dvd_antisymm (order_dvd_exponent _)
  refine Nat.dvd_of_primeFactorsList_subperm he ?_
  rw [List.subperm_ext_iff]
  by_contra! ⟨p, hp, hpe⟩
  replace hp := Nat.prime_of_mem_primeFactorsList hp
  simp only [Nat.primeFactorsList_count_eq] at hpe
  set k := (orderOf t).factorization p with hk
  obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
  suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)
  have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
  have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
    rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
  obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
  have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) := by
    rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
    apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
    nth_rw 1 [← pow_one p]
    have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
      rw [hpk', Nat.factorization_div hpk]
      simp [k, hp]
    rw [this]
    -- Porting note: convert made to_additive complain
    exact Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp
  rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk',
    hg, ha, hk, pow_add, pow_add, pow_one, ← mul_assoc, ← mul_assoc,
    Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ]
  · exact one_lt_pow₀ hp.one_lt a.succ_ne_zero
  · exact hpk

Goal state after:
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
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ (a ^ ↑(orderOf a)) ^ i = 1

Tactic:
zpow_natCast,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ (a ^ orderOf a) ^ i = 1
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
⊢ rank G = 0 ↔ Subsingleton G

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rank_eq_zero G⟩
  obtain ⟨s, hs, hs'⟩ := rank_spec G
  rw [h, Finset.card_eq_zero] at hs
  simpa [hs, subsingleton_iff_bot_eq_top] using hs'

Goal state after:
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; rfl

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
⊢ IsOfFinOrder g

Tactic:
obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = f.ker
tH : IsMulTorsion H
tN : IsMulTorsion ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : f g ^ ngn = 1
⊢ IsOfFinOrder g
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ * x_1)^[n] 1) = ↑1

Tactic:
dsimp
      rw [mul_left_iterate]
      change _ * 1 = 1
      rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯
Q : Subgroup G := ⋯
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ mapSurjective hf (hpQ.toSylow hQ) = P

Tactic:
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, eq_comm]

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ↑P = map f ↑(hpQ.toSylow hQ)
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
let u : Set α := ⋃ i, ⋃ hi : i ∈ s, t i hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
⊢ sSup {a | IsAtom a} = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
⊢ Nat.card G ∣ ∏ g, orderOf g

Tactic:
by
  classical
  refine Nat.dvd_iff_prime_pow_dvd_dvd .. |>.mpr fun p k hp h ↦ ?_
  have := Fact.mk hp
  have ⟨H, hH⟩ := exists_subgroup_card_pow_prime p h
  have (g : G) (hg : g ∈ (H \ {1} : Set G).toFinset) : p ∣ orderOf g := by
    have ⟨hg, hg1⟩ : g ∈ H ∧ g ≠ 1 := by simpa using hg
    simpa using IsPGroup.of_card hH |>.dvd_orderOf (g := ⟨g, hg⟩) <| by simpa
  grw [← prod_dvd_prod_of_subset _ _ _ (H \ {1} : Set G).toFinset.subset_univ,
    ← prod_dvd_prod_of_dvd _ _ this, prod_const, k.le_sub_one_of_lt <| k.lt_pow_self hp.one_lt]
  simp [Finset.card_sdiff, ← Nat.card_eq_fintype_card, hH]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: 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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ ∀ (x y : G), x ∈ P ↑⟨p₁, hp₁⟩ → y ∈ P ↑⟨p₂, hp₂⟩ → Commute x y

Tactic:
have hne' : p₁ ≠ p₂ := by simpa using hne

Goal state after:
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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ ∀ (x y : G), x ∈ P ↑⟨p₁, hp₁⟩ → y ∈ P ↑⟨p₂, hp₂⟩ → Commute x y
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.left
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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ (Fintype.card ↥↑(P ↑⟨p₁, hp₁⟩)).Coprime (Fintype.card ↥↑(P ↑⟨p₂, hp₂⟩))

Tactic:
have hne' : p₁ ≠ p₂ := by simpa using hne

Goal state after:
case refine_2.left
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 ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ (Fintype.card ↥↑(P ↑⟨p₁, hp₁⟩)).Coprime (Fintype.card ↥↑(P ↑⟨p₂, hp₂⟩))
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✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ IsCoatom f.ker

Tactic:
rw [← isSimpleModule_iff_isCoatom]
  exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)

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

Goal state before:
pp: case refine_2.mpr.refine_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) + ↑⟨v, ⋯⟩ = u * 1 + v

Tactic:
← hμ,

Goal state after:
case refine_2.mpr.refine_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) + ↑⟨v, ⋯⟩ = u * ∑ i ∈ t, ↑(μ i) + v
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
h : torsionBySet R M s = ⊤
x : M
⊢ ∀ ⦃a : ↑s⦄, ↑a • x = 0

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
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ torsionBySet R M s
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R[X]
g : PolynomialModule R M
n : ℕ
⊢ (f • g).coeff n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g.coeff x.2

Tactic:
by
  induction f using Polynomial.induction_on' with
  | add p q hp hq => simp [add_smul, hp, hq, ← Finset.sum_add_distrib]
  | monomial f_n f_a =>
    rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j =>
      (monomial f_n f_a).coeff i • g.coeff j, monomial_smul_apply]
    simp [Polynomial.coeff_monomial]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w : f i ≫ colimit.ι (Discrete.functor Y) { as := i } = g i ≫ colimit.ι (Discrete.functor Y) { as := i }
⊢ f i = g i

Tactic:
exact Mono.right_cancellation _ _ w

Goal state after:
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
e : X ≅ Y
p : I → J
inst✝ : X.HasMap p
j : J
⊢ HasCoproduct (Y.mapObjFun p j)

Tactic:
have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)

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
e : X ≅ Y
p : I → J
inst✝ : X.HasMap p
j : J
α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j)
⊢ HasCoproduct (Y.mapObjFun p j)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁
h₂ :
  D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) y₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y₁
⊢ D.tensorProductTo (x₁ * y) + D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y₁ • D.tensorProductTo y +
      ((TensorProduct.lmul' R) y • D.tensorProductTo x₁ + (TensorProduct.lmul' R) y • D.tensorProductTo y₁)

Tactic:
h₁,

Goal state after:
case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁
h₂ :
  D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) y₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y₁
⊢ (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁ +
      D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y₁ • D.tensorProductTo y +
      ((TensorProduct.lmul' R) y • D.tensorProductTo x₁ + (TensorProduct.lmul' R) y • D.tensorProductTo y₁)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) + D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
        (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      ((TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂) +
        (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂))

Tactic:
h₁,

Goal state after:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
        (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂) +
      D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
        (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      ((TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂) +
        (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂))
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₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Goal state after:
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₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Goal state after:
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₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Goal state after:
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₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj { as := n })).hom.app X =
    (MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj { as := n }) ≫
          (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as { as := n }.as).symm.hom ≫
            (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor { as := n }).hom).app
      X

Tactic:
simp [h.zero_add_inv_app, ← Functor.map_comp]

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

Goal state before:
pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
apply Submodule.subset_span

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Tactic:
by
  symm
  rw [Iso.app_inv, Iso.app_hom]
  apply NatIso.naturality_2

Goal state after: