mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x ↦ ↑x.1 \ ↑x.2) hx

Tactic:
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x ↦ ↑x.1 \ ↑x.2) hx
hxt : ((insert x t).sup fun x ↦ ↑x.1 \ ↑x.2) ∈ closure s
⊢ p ((insert x t).sup fun x ↦ ↑x.1 \ ↑x.2) hxt
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
hf : ∅.Finite
ho : ∀ t ∈ ∅, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ ∅, IsCompact t
⊢ IsCompact (⋂₀ ∅)

pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)

Tactic:
· simp [CompactSpace.isCompact_univ]

Goal state after:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
isGenericPoint_def,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ closure {f x} = closure (f '' S)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) univ

Tactic:
by
  simpa using! (IrreducibleSpace.isIrreducible_univ α).isGenericPoint_genericPoint_closure

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
x : α
⊢ {↑(ofComponent ⟨irreducibleComponent x, ⋯⟩)} ⊆ genericPoints α

Tactic:
exact Set.singleton_subset_iff.mpr (ofComponent _).2

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) ∈ I ^ 2

Tactic:
pow_two

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) ∈ I * I
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) ∈ I ^ 2

Tactic:
pow_two

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) ∈ I * I
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if b.factorization p ≤ a.factorization p then p ^ n else 1) *
      if b.factorization p ≤ a.factorization p then 1 else p ^ n) =
    p ^ n

Tactic:
split_ifs

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : b.factorization p ≤ a.factorization p
⊢ p ^ n * 1 = p ^ n

case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
h✝ : ¬b.factorization p ≤ a.factorization p
⊢ 1 * p ^ n = p ^ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))

pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))

Tactic:
· exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩

Goal state after:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))

Tactic:
· exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
| Ideal.span s = ⊤

Tactic:
rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
| ⨆ i, basicOpen ↑i = ⊤
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]
              simp_rw [← vadd_iterate]
              exact isPeriodicPt_minimalPeriod (a +ᵥ ·) b

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ σ ((fun x ↦ h ^ x) n) = (fun x ↦ h ^ x) n ^ m

Tactic:
map_zpow,

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ σ h ^ n = (fun x ↦ h ^ x) n ^ m
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
⊢ Submonoid.powers g = ⊤

Tactic:
ext x
  simp [mem_powers_of_prime_card h hg]

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

Goal state before:
pp: case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = orderOf a

Tactic:
rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]

Goal state after:
case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
h : ¬(k % ↑(Nat.find hex)).natAbs = 0
⊢ ↑(k % ↑(Nat.find hex)).natAbs < ↑(Nat.find hex)

Tactic:
rw [← hk₄]; exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1)

Goal state after:
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:
by
          rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
          exact hm.elim' 1

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑s)ᶜ

Tactic:
exact isRetrocompact_zeroLocus_compl s.finite_toSet

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
d : ℕ
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
⊢ #{a | orderOf a = d} = φ d

Tactic:
induction d using Nat.strong_induction_on with | _ d IH
  rcases Decidable.eq_or_ne d 0 with (rfl | hd0)
  · cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)
  rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩
  have ha : orderOf a = d := (mem_filter.1 ha').2
  have h1 :
    (∑ m ∈ d.properDivisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.properDivisors, φ m := by
    refine Finset.sum_congr rfl fun m hm => ?_
    simp only [mem_properDivisors] at hm
    refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
    rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
  have h2 :
    (∑ m ∈ d.divisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.divisors, φ m := by
    rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
  simpa [← cons_self_properDivisors hd0, ← h1] using h2

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:
simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj]

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ rank ↥(closure s) ≤ s.toFinset.card

Tactic:
← rank_congr (congr_arg _ s.coe_toFinset)

Goal state after:
G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ rank ↥(closure ↑s.toFinset) ≤ s.toFinset.card
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ 1 ^ p ^ m = 1

Tactic:
one_pow

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
a b : G
x✝¹ : a ∈ {g | ∃ k, g ^ p ^ k = 1}
x✝ : b ∈ {g | ∃ k, g ^ p ^ k = 1}
m : ℕ
hm : a ^ p ^ m = 1
n : ℕ
hn : b ^ p ^ n = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
⊢ 1 ∈ ⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
Submodule.mem_iSup_finset_iff_exists_sum

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ (g ^ n) = f₂ (g ^ n)

Tactic:
map_zpow,

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ g ^ n = f₂ (g ^ n)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ g ^ n = f₂ (g ^ n)

Tactic:
map_zpow,

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ g ^ n = f₂ g ^ n
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
⊢ Unique (Sylow p G)

Tactic:
refine { uniq := fun Q ↦ ?_ }

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
⊢ Q = default
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s

Tactic:
by_cases h : x = s.last

Goal state after:
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : x = last s
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s

case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : ¬x = last s
⊢ x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s
Module: Mathlib.Order.JordanHolder

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

Tactic:
ext x
  simp only [mem_snoc, mem_eraseLast h, ne_eq]
  by_cases h : x = s.last <;> simp [*, s.last_mem]

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

Goal state before:
pp: case refine_2.mpr.refine_2.inl
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
t : Finset ι
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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
ij : j ≠ i
hat : j ∉ t
Hb : ∀ b ∈ ↑t, j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
hi : ¬i = j
hj : j ∈ Finset.cons j t hat
⊢ u * ↑(μ i) ∈ I j

Tactic:
exact mul_mem_right _ _ hu

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
⊢ s₁.Equivalent s₂

Tactic:
by
  induction hle : s₁.length generalizing s₁ s₂ with
  | zero => rw [eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht hle]
  | succ n ih =>
    have h0s₂ : 0 < s₂.length :=
      length_pos_of_head_eq_head_of_last_eq_last_of_length_pos hb ht (hle.symm ▸ Nat.succ_pos _)
    rcases exists_last_eq_snoc_equivalent s₁ s₂.eraseLast.last
        (ht.symm ▸ isMaximal_eraseLast_last h0s₂)
        (hb.symm ▸ s₂.head_eraseLast ▸ head_le_of_mem (last_mem _)) with
      ⟨t, htb, htl, htt, hteq⟩
    have := ih t s₂.eraseLast (by simp [htb, ← hb]) htt (Nat.succ_inj.1 (htl.trans hle))
    refine hteq.trans ?_
    conv_rhs => rw [eq_snoc_eraseLast h0s₂]
    simp only [ht]
    exact Equivalent.snoc this (by simpa [htt] using iso_refl)

Goal state after:
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
hn : N.FG
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
rw [fg_def] at hn

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
hn : ∃ S, S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 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
P Q : Ideal R
hc : P ⊔ Q = ⊤
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)

Tactic:
let map : Fin 2 → Ideal R | 0 => P | 1 => Q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)
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
P Q : Ideal R
hc : P ⊔ Q = ⊤
⊢ Disjoint (torsionBySet R M ↑P) (torsionBySet R M ↑Q)

Tactic:
let map : Fin 2 → Ideal R | 0 => P | 1 => Q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ Disjoint (torsionBySet R M ↑P) (torsionBySet R M ↑Q)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P

Tactic:
h1

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ N'
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: A : Type u_3
inst✝ : AddCommGroup A
n : ℤ
⊢ A[-n] = A[n]

Tactic:
by
  ext a
  simp

Goal state after:
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 * I ≤ I ^ 2

Tactic:
pow_two

Goal state after:
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 * I ≤ I * I
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ ↑(x • m) ∈ I ^ 2

Tactic:
pow_two

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ ↑(x • m) ∈ I * I
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I ^ 2

Tactic:
pow_two

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I * I
Module: Mathlib.Algebra.Homology.ComplexShape

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

Tactic:
c₁.next_eq w₁ w₁'

Goal state after:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : c₁.Rel i✝ k
k' : ι
w₂ : c₂.Rel k' j✝
w₁' : c₁.Rel i✝ k'
w₂' : c₂.Rel k' j'✝
⊢ j✝ = j'✝
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      ((δ F (m₁ ⊗ m₂) m₃).app X ≫
          (F.obj m₃).map ((δ F m₁ m₂).app X) ≫
            𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
              (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X) ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app_assoc, μ_δ_app,
    endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

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 L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
⊢ g = h

Tactic:
by
    ext i
    rw [← cancel_mono (φ.f i)]
    exact congr_hom eq i

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
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ ↑⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ - ↑(a • ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) ∈
    ideal R S ^ 2

Tactic:
pow_two

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)
⊢ ↑⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ - ↑(a • ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) ∈
    ideal R S * ideal R S
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁹ : Category.{v, u} V
inst✝⁸ : Preadditive V
W : Type u_2
inst✝⁷ : Category.{v_1, u_2} W
inst✝⁶ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{v_2, u_3} W₁
inst✝⁴ : Category.{v_3, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i : ι
F G : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : G.PreservesZeroMorphisms
α : F ≅ G
c : ComplexShape ι
⊢ NatTrans.mapHomologicalComplex α.hom c ≫ NatTrans.mapHomologicalComplex α.inv c = 𝟙 (F.mapHomologicalComplex c)

Tactic:
simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id,
    NatTrans.mapHomologicalComplex_id]

Goal state after: