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

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
hI : I.IsProper
⊢ ∃ J, I ≤ J ∧ J.IsMaximal

Tactic:
by
  rcases IsCoatomic.eq_top_or_exists_le_coatom I with rfl | ⟨J, hJ, hJ'⟩
  · simp [isProper_iff_ne_top] at hI
  · exact ⟨J, hJ', isMaximal_iff_isCoatom.2 hJ⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff.insert
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝¹ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i_1 ∈ insert i s, b i_1 \ ⋃ i ∈ t, b i) ⋯

Tactic:
simp_rw [biUnion_insert]

Goal state after:
case sdiff.insert
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝¹ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P ((b i \ ⋃ i ∈ t, b i) ∪ ⋃ x ∈ s, b x \ ⋃ i ∈ t, b i) ⋯
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
⊢ HasGoingDown R S

Tactic:
apply of_comap_localRingHom_surjective
  intro P hP
  let := Localization.AtPrime.algebraOfLiesOver (P.under R) P
  have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
    rw [RingHom.algebraMap_toAlgebra]
    exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over
  have : Module.FaithfullyFlat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
  apply PrimeSpectrum.comap_surjective_of_faithfullyFlat

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : sInf {I | I.IsMaximal} ≤ I
⊢ I.IsMaximal

Tactic:
← fin.coe_toFinset,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : sInf ↑fin.toFinset ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous ⇑(primeSpectrumProd R S).symm

Tactic:
rw [continuous_sum_dom]

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inl) ∧ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inr)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case pos
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
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ 0 ≠ 0 ↔ ExponentExists G

Tactic:
· tauto

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

pp: case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
· simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b ≠ 0

Tactic:
minimalPeriod_eq_card

Goal state after:
case intro
n : ℕ
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Finite ↑(orbit (↥(zpowers a)) b)
val✝ : Fintype ↑(orbit (↥(zpowers a)) b)
this : Nonempty ↑(orbit (↥(zpowers a)) b)
⊢ Fintype.card ↑(orbit (↥(zpowers a)) b) ≠ 0
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = comap f ⊤
⊢ H = ⊤

Tactic:
exact comap_injective hf h

Goal state after:
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
h : k.natAbs = 0
⊢ g ^ k = 1

Tactic:
Int.natAbs_eq_zero.mp h,

Goal state after:
α : 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
h : k.natAbs = 0
⊢ g ^ 0 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ sᶜ = comap f '' (comap f ⁻¹' s)ᶜ

Tactic:
← Set.preimage_compl,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ sᶜ = comap f '' comap f ⁻¹' sᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ closure (Set.range (comap f)) = Set.univ ↔ RingHom.ker f ≤ nilradical R

Tactic:
closure_range_comap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ zeroLocus ↑(RingHom.ker f) = Set.univ ↔ RingHom.ker f ≤ nilradical R
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)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
by
  cases finite_or_infinite G
  · obtain ⟨n, hn⟩ := iff_card.mp hG
    rw [hn]
    rcases n with - | n
    · exact Or.inl rfl
    · exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩
  · rw [Nat.card_eq_zero_of_infinite]
    exact Or.inr ⟨0, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n m : ℤ
⊢ (∀ (g : G), g ^ (n - m) = 1) ↔ ∀ (g : G), g ^ n = g ^ m

Tactic:
zpow_sub,

Goal state after:
G : Type u
inst✝ : Group G
n m : ℤ
⊢ (∀ (g : G), g ^ n * (g ^ m)⁻¹ = 1) ↔ ∀ (g : G), g ^ n = g ^ m
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
⊢ exponent M₂ ∣ exponent M₁

Tactic:
refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_
  obtain ⟨m₁, rfl⟩ := hf m₂
  rw [← map_pow, pow_exponent_eq_one, map_one]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

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

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

Tactic:
· rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop
    rw [h_cop]
    exact Or.inl le_top

Goal state after:
case neg
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ c = ∑ m ∈ c.divisors, #{a | orderOf a = m}

Tactic:
simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ c = #{x | x ^ c = 1}
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 = ⊤
i : ι
hi : i ∈ s
⊢ ∃ t, f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
replace h := complementedLattice_iff_isAtomistic.mp (h i hi)

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
⊢ ∃ t, f i = sSup t ∧ ∀ a ∈ t, IsAtom a
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) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j
⊢ ↑(μ i) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j

Tactic:
simp only [mem_iInf] at this ⊢

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
⊢ ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
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) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j
⊢ u * ↑(μ i) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j

Tactic:
simp only [mem_iInf] at this ⊢

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
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → u * ↑(μ i) ∈ I i_1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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
⊢ (eraseLast s).length = n

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_3
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ s ⊆ ↑N

Tactic:
rw [← span_le, hs]

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
⊢ Disjoint ((fun i ↦ torsionBySet R M ↑(p i)) i) (T.sup fun i ↦ torsionBySet R M ↑(p i))

Tactic:
rw [disjoint_iff, Finset.sup_eq_iSup,
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]

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
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
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
heq : ⊤.SupIndep fun i ↦ torsionBySet R M ↑(map i)
⊢ Disjoint (torsionBySet R M ↑P) (torsionBySet R M ↑Q)

pp: case refine_1
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
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤

Tactic:
· simpa [Finset.top_eq_univ, Fin.isValue, map] using heq

Goal state after:
case refine_1
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
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: 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
S : Set (I.Filtration M)
i : ℕ
⊢ sInf (N '' S) (i + 1) ≤ sInf (N '' S) i

Tactic:
apply sInf_le_sInf_of_isCoinitialFor _

Goal state after:
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
S : Set (I.Filtration M)
i : ℕ
⊢ IsCoinitialFor (Set.range fun f ↦ ↑f i) (Set.range fun f ↦ ↑f (i + 1))
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
convert! hn₀ (n - n₀)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - n₀)
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
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)),
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl,
    Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
  rfl

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ Submodule.restrictScalars S (ideal R S)

Tactic:
rw [Submodule.span_le]
    rintro _ ⟨s, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

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

Goal state before:
pp: case refine_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
r : S
x : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (fromIdeal R S) ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : r • x ∈ ideal R S), (fromIdeal R S) ⟨r • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
      Submodule.smul_mem _ r hx₂⟩

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

Goal state before:
pp: ι : Type u_1
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 ι
F G H : W₁ ⥤ W₂
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : H.PreservesZeroMorphisms
α : F ⟶ G
β : G ⟶ H
⊢ mapHomologicalComplex (α ≫ β) c = mapHomologicalComplex α c ≫ mapHomologicalComplex β c

Tactic:
by
  cat_disch

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
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').X (n + 2) ≅ (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1) n)).fst

Tactic:
obtain _ | n := n
  · apply eqToIso
    dsimp [mk', mk, of, mkAux, of.d]
    rw [id_comp]
  · exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ PreservesLimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
subst h
      exact preservesLimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k = 0

Tactic:
apply homotopyCofiber.ext_from_X φ j i hij

Goal state after:
case h₁
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ homotopyCofiber.inlX φ j i hij ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k =
    homotopyCofiber.inlX φ j i hij ≫ 0

case h₂
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ homotopyCofiber.inrX φ i ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k = homotopyCofiber.inrX φ i ≫ 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cocycle F G 0
⊢ Cochain.ofHom z.homOf = ↑z

Tactic:
simpa only [Cocycle.ext_iff] using! ofHom_homOf_eq_self z

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
by_cases h : p'' = p
    · subst h
      by_cases h : q = q'' - 1
      · subst h
        obtain rfl : q' = q'' := by lia
        simp only [single_v]
      · rw [single_v_eq_zero', single_v_eq_zero', zero_comp]
        all_goals lia
    · rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h

Tactic:
by
  ext p q hpq
  dsimp
  simp only [map_v, comp_v _ _ h p _ q rfl (by lia), Φ.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ Congruence fun X Y ↦ Relation.EqvGen (HomRel.CompClosure r)

Tactic:
convert! (inferInstance : Congruence (functor r).homRel)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
x✝¹ x✝ : C
⊢ Relation.EqvGen (HomRel.CompClosure r) = (functor r).homRel