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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ f ⁻¹' closure[inst✝¹] (f '' ↑A) = ↑B

Tactic:
h_images_eq,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst✝¹] (f '' ↑A) = closure[inst✝¹] (f '' ↑B)
⊢ f ⁻¹' closure[inst✝¹] (f '' ↑B) = ↑B
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
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)
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) 1 = 0

Tactic:
ext; simp

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
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x

Tactic:
by
  rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o Additive H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditive ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.toAdditive.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃+o H
⊢ (fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : Additive G ≃+o H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : CommMonoid G
inst✝² : PartialOrder G
inst✝¹ : AddCommMonoid H
inst✝ : PartialOrder H
e : G ≃*o Multiplicative H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeRight e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveLeft e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : G ≃+o Additive H
⊢ (fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.TypeTags

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : AddCommMonoid G
inst✝² : PartialOrder G
inst✝¹ : CommMonoid H
inst✝ : PartialOrder H
e : Multiplicative G ≃*o H
⊢ (fun e ↦ { toMulEquiv := AddEquiv.toMultiplicativeLeft e.toAddEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toAddEquiv := MulEquiv.toAdditiveRight e.toMulEquiv, map_le_map_iff' := ⋯ }) e) =
    e

Tactic:
ext; simp

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus ↑(Ideal.span (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s)))) =
    zeroLocus ↑(Ideal.span s)

Tactic:
← Ideal.map,

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus ↑(Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) (Ideal.span s))) = zeroLocus ↑(Ideal.span s)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
x✝ : ∃ s_1, sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ comap f ⁻¹' zeroLocus (⇑f ⁻¹' F) = sᶜ

Tactic:
rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    x • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } y +
      y • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } x

Tactic:
suffices f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0 by simpa [sub_eq_zero, hf _]
    apply hd
    simp [hf _]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • b • D a + a • a • D b = a • D (a * b)

Tactic:
by rw [leibniz, smul_add, add_comm]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
⊢ comap (Pi.evalRingHom R i) q = comap (Pi.evalRingHom R i) q

Tactic:
ext; simp

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ Continuous (sigmaToPi R)

Tactic:
continuous_sigma_iff

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ ∀ (i : ι), Continuous fun a ↦ sigmaToPi R ⟨i, 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
⊢ k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs

Tactic:
by
          rw [Int.natAbs_of_nonneg
              (Int.emod_nonneg _ (Int.natCast_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]

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

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g

Tactic:
rintro ⟨k, rfl⟩
    exact zpowers_le_of_mem <| npow_mem_zpowers g k

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ 1 = e 1

Tactic:
map_one

Goal state after:
G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ 1 = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsClopen s ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h
    exact ⟨e, f, by simp only [h, and_self]⟩
  rintro ⟨e, f, mul, add, rfl⟩
  exact isClopen_basicOpen_of_mul_add e f mul add

Goal state after:
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
m₁ : M₁
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
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
m₁ : M₁
⊢ 1 = 1
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
S : Type u_4
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₁
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
f₁ f₂ : M →+ M₁
⊢ toZModLinearMap n (f₁ + f₂) = toZModLinearMap n f₁ + toZModLinearMap n f₂

Tactic:
ext; simp

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
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z

Tactic:
rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy

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

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ x✝ ∈ ((zmultiplesHom G) g).ker ↔ x✝ ∈ zmultiples ↑(addOrderOf g)

Tactic:
simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
⊢ ¬p ∣ (↑P).index

Tactic:
rw [← relIndex_mul_index le_normalizer, P.coe_coe, ← card_eq_index_normalizer]
  have : (P.subtype le_normalizer).Normal :=
    Subgroup.normal_in_normalizer
  have : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩
  replace hP := not_dvd_index_aux (P.subtype le_normalizer)
  exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = Fintype.card (ZMod (Nat.card G))ˣ

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case 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 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
have : Std.Symm (I · ⊔ I · = ⊤) := { symm i j := sup_comm .. |>.trans }

Goal state after:
case 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 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤
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
Q : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = default
⊢ P = default

Tactic:
← h2

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
x✝ : G
h1 : P = Q
x : G
h2 : P = default
⊢ P = P
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
this : (normalizer ↑(P.subtype ⋯)).Normal → (↑(P.subtype ⋯)).Normal
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P

Tactic:
rw [← (P.subtype _).coe_coe, coe_subtype,
    normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer),
    ← subgroupOf_normalizer_eq (le_normalizer.trans le_normalizer)] at this

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this :
  ((normalizer ↑↑P).subgroupOf (normalizer ↑(normalizer ↑↑P))).Normal → normalizer ↑(normalizer ↑↑P) ≤ normalizer ↑↑P
⊢ normalizer ↑(normalizer ↑P) = normalizer ↑P
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case e'_5.e'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : IsMaximal (s.toFun ⟨s.length - 1, ⋯⟩) (s.toFun ⟨s.length - 1 + 1, ⋯⟩)
⊢ ↑(Fin.last s.length) = s.length - 1 + 1

Tactic:
exact (tsub_add_cancel_of_le h).symm

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 : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : N →ₗ[R] M
hf : Function.Injective ⇑f
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
⊢ (g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f = g

Tactic:
ext; simp

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₂
hs₁ : s₁.length = 0
⊢ s₂.length = 0

Tactic:
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm
  simpa [Fin.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m₁ m₂ : M
⊢ single R n (m₁ + m₂) = single R n m₁ + single R n m₂

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : ↥((Algebra.lsmul R R M) a).invtSubmodule
⊢ (fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩)
      ((fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
        p) =
    p

Tactic:
ext; simp

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

Goal state before:
pp: case empty
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
s : Set M
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R ∅)
right✝ : ∅ ⊆ ↑N
n : M
hn : n ∈ N
⊢ r • n = 0

Tactic:
specialize hrn hn

Goal state after:
case empty
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
s : Set M
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : n ∈ comap ((LinearMap.lsmul R M) r) (I • span R ∅)
hn : n ∈ N
⊢ r • n = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
f : R[X]
m : M
n : ℕ
⊢ (f • single R i m).coeff n = if i ≤ n then f.coeff (n - i) • m else 0

Tactic:
by
  induction f using Polynomial.induction_on' with
  | add p q hp hq => simp [add_smul, hp, hq, ite_add_ite]
  | monomial => simp; grind [monomial_smul_single, coeff_monomial, zero_smul]

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

Goal state before:
pp: case insert.refine_2
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
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
specialize hrn hn

Goal state after:
case insert.refine_2
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
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : n ∈ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ r ^ (n✝ + i) • a✝ • m = (a✝ * r ^ n✝) • r ^ i • m

Tactic:
module

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
r : R
i : ℕ
m : M
⊢ (algebraMap R R') r ^ i • f m = r ^ i • f m

Tactic:
module

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ Polynomial.eval r p ^ i • r ^ 0 • m = Polynomial.eval r p ^ i • m

Tactic:
module

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
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'
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N

Tactic:
have h1 : P.map N.mkQ = N'.map N.mkQ := by
    refine le_antisymm ?_ (map_mono hN'le)
    simpa using map_mono (f := N.mkQ) hNN''

Goal state after:
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'
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N
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
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'
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N

Tactic:
have h2 : P.map N.mkQ = (I • N').map N.mkQ := by
    apply le_antisymm
    · simpa using map_mono (f := N.mkQ) hNN'
    · rw [h1]
      simp [smul_le_right]

Goal state after:
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')
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
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 = ⊤
hs_span' : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤
⊢ ⊤.spanRank ≤ ⊤.spanRank

Tactic:
← hs_card,

Goal state after:
case a
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 = ⊤
hs_span' : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤
⊢ ⊤.spanRank ≤ Cardinal.mk ↑s
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ ⊤.spanRank ≤ ⊤.spanRank

Tactic:
← hs_card,

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ ⊤.spanRank ≤ Cardinal.mk ↑s
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : DecidableEq α
inst✝ : One α
⊢ DecidableRel (up α).Rel

Tactic:
by
  dsimp [ComplexShape.up]; infer_instance

Goal state after: