mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
s : Set X
⊢ ⋃ i, s ∩ ↑(u i) = s

Tactic:
by
  simp [← inter_iUnion, hu.iSup_set_eq_univ]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : GeneralizingMap f
s : Set β
x : ↑(f ⁻¹' s)
y : ↑s
h : y ⤳ s.restrictPreimage f x
a : α
ha : a ⤳ ↑x
hy : f a = ↑y
⊢ a ∈ f ⁻¹' s

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsBasis B
f : α → β
h : IsInducing f
⊢ IsBasis {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x}

Tactic:
simp only [IsBasis] at H ⊢
  convert! H.isInducing h
  ext; simp

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨?_, fun H ι U hU => ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ t.sup U
Module: Mathlib.Topology.Spectral.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
U : Set ((i : ι) × X i)
hU : U ∈ ⋃ i, (fun u ↦ Sigma.mk i '' u) '' {U | IsOpen[inst✝¹ i] U ∧ IsCompact U}
⊢ IsCompact U

Tactic:
by
    simp_rw [Set.mem_iUnion] at hU
    obtain ⟨i, V, hV, rfl⟩ := hU
    exact hV.2.image continuous_sigmaMk

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G

Tactic:
split_ifs with h

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ Nat.find h ≠ 0 ↔ ExponentExists G

case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ 0 ≠ 0 ↔ ExponentExists G
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 : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ ↑n ∈ ⊥

Tactic:
mem_bot,

Goal state after:
n✝ : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
q : ℤ ⧸ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)
n : ℤ
hn :
  ↑n ∈
    (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker
⊢ ↑n = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
have := card_subgroup_dvd_card H

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : Nat.card ↥H ∣ Nat.card G
⊢ H = ⊥ ∨ H = ⊤
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩

Tactic:
by
  rw [← eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ orderOf g = Nat.card α

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers]

Goal state after:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ ∀ (x : α), x ∈ zpowers g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I

Tactic:
· obtain ⟨q, hqI, hq, hqle⟩ := p.asIdeal.exists_ideal_comap_le_prime I hp
    exact hf ((le_iff_specializes ⟨q.comap f, inferInstance⟩ p).mp hqle) ⟨⟨q, hq⟩, hqI, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
simp_rw [← isMin_iff, StableUnderGeneralization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ a ≤ x, a = x) ↔ IsMin x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ orderOf y = (orderOf x).lcm (orderOf y)

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : ¬(Set.range orderOf).Finite ↔ exponent G = 0
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
Iff.comm

Goal state after:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G = 0 ↔ ¬(Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Nat.card_eq_fintype_card, ← ZMod.intCast_eq_intCast_iff] at hy

Goal state after:
case refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : ↑n = ↑↑y.val
⊢ y = ↑n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g

Tactic:
split_ifs with h

Goal state after:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ univ.lcm fun x ↦ exponent (M x)
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤

Tactic:
rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ←
      Fintype.univ_bool]

Goal state after:
α : Type u_1
β : Type u_2
a : Bool
⊢ a ∈ Finset.univ
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ K = ⊤

Tactic:
rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]

Goal state after:
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:
by
  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.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
⊢ Subsingleton ↥N ∨ ∃ m ≤ N, IsSimpleModule R ↥m

Tactic:
← Submodule.subsingleton_iff R,

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
⊢ Subsingleton (Submodule R ↥N) ∨ ∃ m ≤ N, IsSimpleModule R ↥m
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
simp [add_smul, hp, hq, ← Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
⊢ (if i = 0 then 1 else 0) ∈ I ^ i

Tactic:
split_ifs with h

Goal state after:
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : i = 0
⊢ 1 ∈ I ^ i

case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ (if i = 0 then (algebraMap R R) r else 0) ∈ I ^ i

Tactic:
split_ifs with h

Goal state after:
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : i = 0
⊢ (algebraMap R R) r ∈ I ^ i

case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
mem_bot,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x = 0
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N' ≤ N

Tactic:
by
  rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]

Goal state after:
Module: Mathlib.RingTheory.Filtration

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
F : I.Filtration M
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ (if i = j then m else 0) ∈ F.N j

Tactic:
split_ifs with h

Goal state after:
case pos
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
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : i = j
⊢ m ∈ F.N j

case neg
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
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
h : ¬i = j
⊢ 0 ∈ F.N j
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ d ((CommRingCat.Hom.hom f) 1) = 0

Tactic:
d_map

Goal state after:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑A ↑A' ↑B' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑A ↑B'))
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)

Goal state after:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑A ↑A' ↑B' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑A ↑B'))
this : IsScalarTower ↑A ↑B ↑B'
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ a ∈ RingHom.ker f.toRingHom ^ 2, f.toRingHom a = 0

pp: case refine_2
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (r : R),
    (↑↑(Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ?refine_1)).toFun
        ((algebraMap R (A ⧸ RingHom.ker f.toRingHom ^ 2)) r) =
      (algebraMap R B) r

Tactic:
· intro a ha; exact Ideal.pow_le_self two_ne_zero ha

Goal state after:
case refine_2
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (r : R),
    (↑↑(Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ⋯)).toFun
        ((algebraMap R (A ⧸ RingHom.ker f.toRingHom ^ 2)) r) =
      (algebraMap R B) r
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (maximalIdeal R).toCotangent (Submodule.map (maximalIdeal R).toCotangent M))

Tactic:
H,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) (Submodule.comap (maximalIdeal R).toCotangent ⊤)
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Tactic:
Ideal.toCotangent_range

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ ⊤ = ⊤
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (n + m) • s = x✝ + n • s + m • s

Tactic:
add_zsmul,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (n • s + m • s) = x✝ + n • s + m • s
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 : V
i✝ : ι
⊢ (if h : i✝ = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0) = 𝟙 (if i✝ = j then A else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : i✝ = j
⊢ eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ = 𝟙 (if i✝ = j then A else 0)

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ 0 = 𝟙 (if i✝ = j then A else 0)
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 : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
⊢ (if h : i✝ = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0) =
    (if h : i✝ = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫ if h : i✝ = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0

Tactic:
split_ifs with h

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
h : i✝ = j
⊢ eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ = (eqToHom ⋯ ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ g ≫ eqToHom ⋯

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
h : ¬i✝ = j
⊢ 0 = 0 ≫ 0
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 Y Z : Discrete A),
    MonoidalCategoryStruct.whiskerRight (h.add X.as Y.as).symm.hom ((Discrete.functor h.F).obj Z) ≫
        (h.add (MonoidalCategoryStruct.tensorObj X Y).as Z.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.associator X Y Z).hom =
      (MonoidalCategoryStruct.associator ((Discrete.functor h.F).obj X) ((Discrete.functor h.F).obj Y)
            ((Discrete.functor h.F).obj Z)).hom ≫
        MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj X) (h.add Y.as Z.as).symm.hom ≫
          (h.add X.as (MonoidalCategoryStruct.tensorObj Y Z).as).symm.hom

Tactic:
rintro ⟨m₁⟩ ⟨m₂⟩ ⟨m₃⟩
        ext X
        simp [h.assoc_inv_app_assoc]

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

Goal state before:
pp: case refine_1
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)
⊢ ∀ x ∈ Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,
    ∃ (hx : x ∈ ideal R S), (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rintro _ ⟨x, rfl⟩
    refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
    apply Submodule.subset_span
    exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩

Goal state after: