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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑p'.length + (↑p.length - ↑↑i) ≤ ↑p.length
⊢ ↑p'.length ≤ ↑↑i

Tactic:
norm_cast at *

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : p'.length + (p.length - ↑i) ≤ p.length
⊢ p'.length ≤ ↑i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ r.InfiniteDimensional

Tactic:
infiniteDimensional_iff

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lg) g ⋯
leq : ↑lf = ↑lg
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩

Tactic:
Fin.val_eq_val

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin (↑lg + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lg) g ⋯
leq : lf = lg
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lg, g⟩, mg⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), f i = (mk (↑lf) g ⋯).toFun i
⊢ f = g

Tactic:
mk_toFun lf g mg,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), f i = g i
⊢ f = g
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ⨆ x, ↑(↑x).length = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
ENat.iSup_natCast_eq_top,

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬BddAbove (Set.range fun x ↦ (↑x).length)
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
simp; lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ⨆ x_1, ↑(↑x_1).length = ⊤

Tactic:
ENat.iSup_natCast_eq_top,

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬BddAbove (Set.range fun x_1 ↦ (↑x_1).length)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
· suffices ∃ x < a, ↑n ≤ height x by
      simp_all [minimal_iff_forall_lt]
    simp only [top_le_iff, height_eq_top_iff] at hfin
    obtain ⟨p, rfl, hp⟩ := hfin (n + 1)
    use p.eraseLast.last, p.eraseLast_last_rel_last (by lia)
    simpa [hp] using length_le_height_last (p := p.eraseLast)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ¬IsEmpty α ↔ Nonempty α

Tactic:
not_isEmpty_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ Nonempty α ↔ Nonempty α
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : P →ₗ[R] M ⊗[R] N
⊢ ↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) ∘ₗ f = f

Tactic:
rw [← LinearMap.comp_assoc, comm_comp_comm, LinearMap.id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : Module R P
inst✝ : Module R Q
g✝ : P →ₗ[R] Q
f✝ f g : N →ₗ[R] P
⊢ lTensor M (f + g) = lTensor M f + lTensor M g

Tactic:
by
    ext x y
    simp only [compr₂ₛₗ_apply, mk_apply, add_apply, lTensor_tmul, tmul_add]

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

Goal state before:
pp: case e'_3.e'_5
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

pp: case e'_3.e'_6
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * ∏ j ∈ insert a t \ {x}, s j = (μ * fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
· by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]

Goal state after:
case e'_3.e'_6
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * ∏ j ∈ insert a t \ {x}, s j = (μ * fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)

Tactic:
rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑(opLinearEquiv R) (m * n) ∈ comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M

pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)

Tactic:
· simp_rw [map_le_iff_le_comap]
    refine mul_le.2 fun m hm n hn => ?_
    rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
    change op n * op m ∈ _
    exact mul_mem_mul hn hm

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ s a * ∏ x ∈ r, s x ∣ z

Tactic:
refine
        (IsRelPrime.prod_right fun i hir ↦
              Hs aux1 (Finset.mem_insert_of_mem hir) <| by
                rintro rfl
                exact har hir).mul_dvd
          (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ ↑r ⊆ ↑(insert a r)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s * t) • P = s • t • P

Tactic:
by
    simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) ∉ I.prod J

Tactic:
by simp [hJ]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Type u_7} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsNoetherian R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : β → Type u_7} [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)]
        [∀ (i : β), IsNoetherian R (M i)], IsNoetherian R ((i : β) → M i)

Tactic:
exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
x : R
hx : x ∈ s
⊢ f x ∈ ↑(map f (span s))
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p

Tactic:
hq,

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : 0 ∣ p
hq : q = 0
⊢ p / q ∣ p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y - z / t = (t * x - y * z) / (t * y)

Tactic:
by
  apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
  rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).annihilator = ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
ext; simp [mem_annihilator_span]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ (∅ ∪ s₂).lcm f = GCDMonoid.lcm (∅.lcm f) (s₂.lcm f)

Tactic:
by rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ f (f_inv 1) - f 1 = 0

Tactic:
sub_eq_zero,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ f (f_inv 1) = f 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m

Tactic:
rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup]
  apply Finset.sup_le
  intro i hi
  by_cases hn : n ≤ i
  · exact (Ideal.mul_le_left.trans (Ideal.mul_le_left.trans
      ((Ideal.pow_le_pow_right hn).trans le_sup_left)))
  · refine (Ideal.mul_le_left.trans (Ideal.mul_le_right.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))
    lia

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ f (f_inv (x * y)) - f (f_inv x * f_inv y) = 0

Tactic:
sub_eq_zero,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ f (f_inv (x * y)) = f (f_inv x * f_inv y)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ (∏ i ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_prod_eq_top]

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
simp [normUnit_mul_units _ h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ normalize (normalize x) = normalize x

Tactic:
simp [normalize_apply]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ s.gcd f

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1

Tactic:
· apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      grw [hd₁, hab.dvd]

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

Goal state before:
pp: case h.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : a = 0
h : a * b = c ^ 0
⊢ Associated (0 ^ 0) a

Tactic:
simp [ha] at h

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
⊢ a ≠ 0

Tactic:
by
  rintro rfl
  simp at h

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
  · exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)
  · by_contra H
    exact
      h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
        (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊤

Tactic:
· apply top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
r : R
⊢ Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}

Tactic:
exact Ideal.span_singleton_generator _

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ normalize c

Tactic:
apply dvd_normalize_iff.2 ac

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa using congrFun₂ h (Pi.single j 1) i

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ (1 • s).toFinset = s.toFinset

Tactic:
one_nsmul

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ s.toFinset = s.toFinset
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}

Tactic:
refine ⟨fun H ↦ ⟨fun h ↦ ?_, ext' fun x ↦ ?_⟩, fun H ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Equivalence fun x y ↦ f x = f y

Tactic:
constructor <;> aesop

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Tactic:
by
  simp only [iSup, sSup_ringCon]; congr; ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S

Tactic:
cases S; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
cases S; rfl

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ adjoin R ({(algebraMap R A) x} ∪ s) = adjoin R s

Tactic:
adjoin_union

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
s : Set A
⊢ R[(algebraMap R A) x] ⊔ adjoin R s = adjoin R s
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ center.instNonUnitalCommSemiring.toNonUnitalSemiring = NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A)

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
| g p

Tactic:
rw [← hs p]

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
| g ((linearCombination R id) (s p))