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

Goal state before:
pp: case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u

Tactic:
intro x sU hx hsU

Goal state after:
case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst✝] sU
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
s : Set β
⊢ IsClosed[inst✝] s ↔ ∀ (i : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)

Tactic:
simpa using hU.isOpen_iff_coe_preimage (s := sᶜ)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case insert.inr
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
hne : s.Nonempty
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)

Tactic:
grind [IsCompact.inter_of_isOpen, hs.isOpen_sInter, Set.sInter_insert]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I

Tactic:
induction s, hs using Finite.induction_on with simp [↓iSup_insert, sup_mem_iff, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ range toCompacts = {⊥}ᶜ

Tactic:
by
  ext K
  rw [mem_compl_singleton_iff, ← Compacts.coe_nonempty]
  refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩
  rintro ⟨K, rfl⟩
  exact K.nonempty

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝²] U
hUs : IsConstructible (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst✝²] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (V ↓∩ s)
⊢ IsRetrocompact (range Subtype.val)

Tactic:
by simpa using hV₂.isRetrocompact hV₁

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : x ∉ I
y : R
hy : y ∈ t
⊢ y ∈ I

Tactic:
exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Goal state after:
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
⊢ zpowers g = ⊤

Tactic:
subst h
  have := (zpowers g).eq_bot_or_eq_top_of_prime_card
  rwa [zpowers_eq_bot, or_iff_right hg] at this

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.univ.lcm orderOf ∣ exponent G

Tactic:
apply Finset.lcm_dvd
  intro g _
  exact order_dvd_exponent g

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
k : ℤ
h : zpowers (g ^ k) ≤ zpowers g
⊢ ∃ n, zpowers (g ^ k) = zpowers (g ^ n)

Tactic:
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg k

Goal state after:
case refine_1.inl
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ ↑n) = zpowers (g ^ n_1)

case refine_1.inr
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ (-↑n)) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ (-↑n)) = zpowers (g ^ n_1)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_1.inl
G : Type u_2
inst✝ : Group G
g : G
n : ℕ
h : zpowers (g ^ ↑n) ≤ zpowers g
⊢ ∃ n_1, zpowers (g ^ ↑n) = zpowers (g ^ n_1)

Tactic:
exact ⟨n, by rw [zpow_natCast]⟩

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 : 0 < m
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd (n.gcd (Fintype.card α) * m / n.gcd (Fintype.card α)) ≤ n

Tactic:
Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0),

Goal state after:
α : 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 : 0 < m
⊢ Fintype.card α / (n.gcd (Fintype.card α) * m).gcd m ≤ n
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl.refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ 0 * 0 = 0

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case inl.refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ 0 + 0 = 1

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case inl.refine_3
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ s = ↑(basicOpen 0)

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case inl.refine_4
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ sᶜ = ↑(basicOpen 0)

Tactic:
apply Subsingleton.elim

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
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ f.IsIntegral

Tactic:
rwa [Algebra.isIntegral_def] at this

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (c • x) = c • f x

Tactic:
← ZMod.intCast_zmod_cast c

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
⊢ f.IsIntegral

Tactic:
algebraize [f]
  suffices Algebra.IsIntegral R S by rwa [Algebra.isIntegral_def] at this
  nontriviality R
  nontriviality S
  constructor
  intro r
  let p : S[X] := C r * X - 1
  have : (1 : R[X]) ∈ Ideal.span {X} ⊔ (Ideal.span {p}).comap (mapRingHom f) := by
    have H := h _ (isClosed_zeroLocus {p})
    rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
    rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
    suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
    intro q hpq hXq
    have : 1 ∈ q.asIdeal := by simpa [p] using! (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
    exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)
  obtain ⟨a, b, hb, e⟩ := Ideal.mem_span_singleton_sup.mp this
  obtain ⟨c, hc : b.map (algebraMap R S) = _⟩ := Ideal.mem_span_singleton.mp hb
  refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
  · refine Monic.mul ?_ (by simp)
    have h : b.coeff 0 = 1 := by simpa using! congr(($e).coeff 0)
    have : b.natTrailingDegree = 0 := by simp [h]
    rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
  · have : p.natDegree ≤ 1 := by simpa using! natDegree_linear_le (a := r) (b := -1)
    rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow,
      map_X, ← revAt_zero (1 + _), ← reflect_monomial,
      ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc,
      ← add_assoc, reflect_mul _ _ (this.trans (by simp)) le_rfl,
      eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
    simp [← pow_succ']

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ G ⧸ stabilizer G P ≃ G ⧸ normalizer ↑P

Tactic:
P.stabilizer_eq_normalizer

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ G ⧸ normalizer ↑P ≃ G ⧸ normalizer ↑P
Module: Mathlib.Order.CompactlyGenerated.Intervals

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

Tactic:
have hu₁ : u ⊆ {a | IsAtom a} := by
    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
    exact ht' i hi a ha

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

Goal state before:
pp: 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
⊢ normalizer ↑↑P = ⊤

Tactic:
rcases eq_top_or_exists_le_coatom (normalizer (P : Set G))
        with (heq | ⟨K, hK, hNK⟩)

Goal state after:
case inl
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
heq : normalizer ↑P = ⊤
⊢ normalizer ↑↑P = ⊤

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
⊢ normalizer ↑↑P = ⊤
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x

Tactic:
by
  rcases Set.mem_range.1 hx with ⟨i, rfl⟩
  rcases Set.mem_range.1 hy with ⟨j, rfl⟩
  rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
  exact le_total i j

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)).castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)).succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc)
            (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length))).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc)
            (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length))).succ)

Tactic:
Equiv.swap_apply_left,

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)).castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun
        (Fin.last ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)).succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last s.length).castSucc.succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ f.ker = ⊥ ∨ f = 0

Tactic:
← ker_eq_top

Goal state after:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ f.ker = ⊥ ∨ f.ker = ⊤
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
⊢ s₁.Equivalent s₂

Tactic:
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⟩

Goal state after:
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
⊢ s₁.Equivalent s₂
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case smul₁
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'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
r✝ : R
m✝ : M
mem✝ : m✝ ∈ r • P
h : m✝ ∈ N
⊢ r✝ • m✝ ∈ N

Tactic:
| smul₁ _ _ _ h =>

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ Function.Surjective ⇑f

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ f.range = ⊤
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
⊢ Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J) ≤
    Submodule.comap J.toCotangent (J.mapCotangent I (Algebra.ofId A B) ⋯).ker

Tactic:
← LinearMap.ker_comp

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
⊢ Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯ ∘ₗ J.toCotangent).ker
Module: Mathlib.CategoryTheory.GradedObject

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

Tactic:
colimit.ι_map

Goal state after:
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  (Discrete.natTrans fun X ↦ (fun i ↦ f i) X.as).app { as := i } ≫
      colimit.ι (Discrete.functor fun i ↦ Y i) { as := i } =
    (Discrete.natTrans fun X ↦ (fun i ↦ g i) X.as).app { as := i } ≫
      colimit.ι (Discrete.functor fun i ↦ Y i) { as := i }
⊢ f i = g i
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
D : Derivation R S M
x y : S ⊗[R] S
⊢ D.tensorProductTo (x * y) =
    (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
  · rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [add_mul, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x₁ x₂
  refine TensorProduct.induction_on y ?_ ?_ ?_
  · rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x y
  simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo,
    TensorProduct.AlgebraTensorModule.lift_apply,
    TensorProduct.lmul'_apply_tmul]
  dsimp
  rw [D.leibniz]
  simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]

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)
⊢ (DLinearMap R S) (a * b) = a • (DLinearMap R S) b + b • (DLinearMap R S) a

Tactic:
dsimp [KaehlerDifferential.DLinearMap_apply]

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)
⊢ (ideal R S).toCotangent ⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ =
    a • (ideal R S).toCotangent ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • (ideal R S).toCotangent ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩
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
⊢ (S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal ≃+* S

Tactic:
have : Function.RightInverse (TensorProduct.includeLeft (R := R) (S := R) (A := S) (B := S))
      (↑(TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S) : S ⊗[R] S →+* S) := by
    intro x; rw [AlgHom.coe_toRingHom, ← AlgHom.comp_apply, TensorProduct.lmul'_comp_includeLeft]
    rfl
  refine (Ideal.quotCotangent _).trans ?_
  refine (Ideal.quotEquivOfEq ?_).trans (RingHom.quotientKerEquivOfRightInverse this)
  ext; rfl

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
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝¹ x✝ : S
hx✝¹ : x✝ ∈ adjoin R ↑(EssFiniteType.finset R S)
x y : S
hx✝ : x ∈ adjoin R ↑(EssFiniteType.finset R S)
hy✝ : y ∈ adjoin R ↑(EssFiniteType.finset R S)
hx : (D R S) x ∈ Submodule.span S ↑s
hy : (D R S) y ∈ Submodule.span S ↑s
⊢ (D R S) (x * y) ∈ Submodule.span S ↑s

Tactic:
simp only [Derivation.leibniz]

Goal state after:
case refine_4
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
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝¹ x✝ : S
hx✝¹ : x✝ ∈ adjoin R ↑(EssFiniteType.finset R S)
x y : S
hx✝ : x ∈ adjoin R ↑(EssFiniteType.finset R S)
hy✝ : y ∈ adjoin R ↑(EssFiniteType.finset R S)
hx : (D R S) x ∈ Submodule.span S ↑s
hy : (D R S) y ∈ Submodule.span S ↑s
⊢ x • (D R S) y + y • (D R S) x ∈ Submodule.span S ↑s
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
⊢ Function.Surjective ⇑(linearCombination S ⇑(D R S))

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).range = ⊤