mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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 / p ^ k).factorization p + 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
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
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k) * orderOf g

Tactic:
hpk',

Goal state after:
case h
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
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf t / p ^ k * orderOf g
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

pp: case neg
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
case neg he =>
    rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

Goal state after:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1

Tactic:
simpa using congr_fun h j

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.comap (algebraMap R S) ⊥ ≤ p

Tactic:
by simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ fixedPoints ↥↑P ↑(orbit G P) = {⟨P, ⋯⟩}

Tactic:
rw [Set.eq_singleton_iff_unique_mem]

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ ⟨P, ⋯⟩ ∈ fixedPoints ↥↑P ↑(orbit G P) ∧ ∀ x ∈ fixedPoints ↥↑P ↑(orbit G P), x = ⟨P, ⋯⟩
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
⊢ ↑(⟨x, ⋯⟩ ^ n) * 1 = 1

Tactic:
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
        (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ exponent α = Nat.card α

Tactic:
apply Nat.dvd_antisymm Group.exponent_dvd_nat_card

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.card ↥f.ker = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M

Tactic:
(f.ofInjective (f.ker_eq_bot_iff.mp (f.ker.eq_bot_of_card_eq h))).isCyclic

Goal state after:
case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.card ↥f.ker = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic ↥f.range
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
⊢ ∃ H' ≤ H, Nat.card ↥H' = p ^ n

Tactic:
obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hn
  refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩
  rw [← H'card]
  let e : H' ≃* H'.map H.subtype := H'.equivMapOfInjective (Subgroup.subtype H) H.subtype_injective
  exact Nat.card_congr e.symm.toEquiv

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

Goal state before:
pp: ι : 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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
⊢ j ∈ t → j ≠ i → ↑(μ i) ∈ I j

Tactic:
hj

Goal state after:
ι : 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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
⊢ j ≠ i → ↑(μ i) ∈ I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case pos
ι : 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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

Tactic:
rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (eraseLast s).last (last s)
hs : s.length = 0
⊢ last s = (eraseLast s).last

Tactic:
by simp [last, Fin.ext_iff, hs]

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

Goal state before:
pp: case refine_2.mpr.refine_1
ι : 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
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
⊢ j ∈ Finset.cons a t hat → j ≠ i → v ∈ I j

Tactic:
hj

Goal state after:
case refine_2.mpr.refine_1
ι : 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
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
⊢ j ≠ i → v ∈ I j
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 : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
x✝ : ∃ a, IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsAtom m
right✝ : m ≤ ⊤
⊢ IsSimpleModule R ↥(Submodule.map N.subtype m)

Tactic:
rw [← isSimpleModule_iff_isAtom] at h

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
x✝ : ∃ a, IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsSimpleModule R ↥m
right✝ : m ≤ ⊤
⊢ IsSimpleModule R ↥(Submodule.map N.subtype m)
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_2
ι : 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 + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
⊢ j ∈ Finset.cons a t hat → j ≠ i → u * ↑(μ i) ∈ I j

Tactic:
hj

Goal state after:
case refine_2.mpr.refine_2
ι : 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 + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
⊢ j ≠ i → u * ↑(μ i) ∈ I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_3.e_a
ι : 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
j : ι
⊢ j ∈ t → ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)

Tactic:
hj

Goal state after:
case refine_2.mpr.refine_3.e_a
ι : 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
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
this : s.Equivalent ((snoc t (eraseLast s).last ⋯).snoc (last s) ⋯)
⊢ s.Equivalent ((snoc t x hmtx).snoc (last s) ⋯)

Tactic:
refine this.trans <| Equivalent.snoc_snoc_swap
        (iso_symm
            (second_iso_of_eq hm
              (sup_eq_of_isMaximal hm (isMaximal_eraseLast_last h0s) (Ne.symm hetx)) htt.symm))
        (second_iso_of_eq (isMaximal_eraseLast_last h0s)
            (sup_eq_of_isMaximal (isMaximal_eraseLast_last h0s) hm hetx) (by rw [inf_comm, htt]))

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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
⊢ j ∈ T → p i ⊔ p j = ⊤

Tactic:
hj

Goal state after:
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ F.N (n + n₀ + 1) ≤ F'.N (n + 1)

Tactic:
← hF

Goal state after:
case h.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ I • F.N (n + n₀) ≤ F'.N (n + 1)

case h.succ.a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ n + n₀ ≥ n₀
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₂ : c₂.Rel k j✝
k' : ι
w₁ : c₁.Rel i✝ k'
w₁' : c₁.Rel i'✝ k'
w₂' : c₂.Rel k' j✝
⊢ i✝ = i'✝

Tactic:
exact c₁.prev_eq w₁ w₁'

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
desc✝¹ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝¹ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝¹ d') = d'
postcomp_injective✝¹ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ }.desc d' =
      { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d'
⊢ { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ } =
    { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }

Tactic:
simp only [Universal.mk.injEq]

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
desc✝¹ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝¹ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝¹ d') = d'
postcomp_injective✝¹ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ }.desc d' =
      { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d'
⊢ desc✝¹ = desc✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (M.map f✝)) ((ConcreteCategory.hom (f.app X✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1

Tactic:
rw [← naturality_apply, unit_map_one]

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ ((single V c j).map f).f j = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
dsimp [single]
  rw [dif_pos rfl]
  rfl

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
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj X) ≫
        (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as X.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor X).hom

Tactic:
rintro ⟨n⟩
        ext X
        simp [h.zero_add_inv_app, ← Functor.map_comp]

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
a b : S
⊢ (DLinearMap R S) (a * b) = a • (DLinearMap R S) b + b • (DLinearMap R S) a

Tactic:
have : LinearMap.CompatibleSMul { x // x ∈ ideal R S } Ω[S⁄R] S (S ⊗[R] S) := inferInstance

Goal state after:
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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (DLinearMap R S) (a * b) = a • (DLinearMap R S) b + b • (DLinearMap R S) a
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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
⊢ f = f'

Tactic:
apply LinearMap.ext
  intro x
  have : x ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) := by
    rw [KaehlerDifferential.span_range_derivation]; trivial
  refine Submodule.span_induction ?_ ?_ ?_ ?_ this
  · rintro _ ⟨x, rfl⟩; exact congr_arg (fun D : Derivation R S M => D x) hf
  · rw [map_zero, map_zero]
  · intro x y _ _ hx hy; rw [map_add, map_add, hx, hy]
  · intro a x _ e; simp [e]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0

Tactic:
· obtain rfl := c.prev_eq' hij
    exact (K.sc j).f_pOpcycles

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ K.d i j ≫ K.pOpcycles j = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
· have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
      rw [K.shape _ _ h, zero_comp] at hx
      rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
    rw [this, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₀) hom + hom k₀ k₁ ≫ D.d k₁ k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
dNext,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (AddMonoidHom.mk' (fun f ↦ C.d k₀ (c.next k₀) ≫ f (c.next k₀) k₀) ⋯) hom + hom k₀ k₁ ≫ D.d k₁ k₀ =
    hom k₀ k₁ ≫ D.d k₁ k₀