mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ∀ (a : Finset V),
    ↑a ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑a ∧ a.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card →
      ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
intro u h

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
h : ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x).coeff m₁ = r * x.coeff m₂

Tactic:
by
  classical
  calc
    (single m r * x).coeff m₁
    _ = x.coeff.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [coeff_mul]
    _ = x.coeff.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by gcongr; simp [*]
    _ = r * x.coeff m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
eq : f * (erase ag g₁ + single ag (g₁.coeff ag)) = f * g₂
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
⊢ erase ag g₁ + single ag (g₁.coeff ag) = g₂

Tactic:
← g₂.erase_add_single ag,

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
eq : f * (erase ag g₁ + single ag (g₁.coeff ag)) = f * (erase ag g₂ + single ag (g₂.coeff ag))
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₂.coeff ag)
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
⊢ Free R' M'

Tactic:
let e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'

Goal state after:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
⊢ Free R' M'
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ span R (Set.range fun x ↦ single (u x) 1) ≤ (lmapDomain R R u).range

Tactic:
rw [Submodule.span_le, Set.range_subset_iff]
    intro i
    exact ⟨Finsupp.single i 1, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
⊢ (a0, b0) ≠ (a, b)

Tactic:
simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc✝ : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
hne : ¬a = a0 ∨ ¬b0 = b
⊢ (a0, b0) ≠ (a, b)
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ ↑L = ∅ ↔ L = ⊥

Tactic:
by rw [← coe_bot, coe_inj]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r * X ^ k = (monomial (n + k)) r
⊢ (monomial n) r * X ^ (k + 1) = (monomial (n + (k + 1))) r

Tactic:
simp [ih, pow_succ, ← mul_assoc, add_assoc]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q

Tactic:
by
  rw [codisjoint_iff, codisjoint_iff, Sublattice.mk_sup_mk,
    Subtype.mk_eq_top_iff (⊤ : f.invtSubmodule).property]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.coeffs.Nonempty

Tactic:
← support_nonempty

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).preimage s

Tactic:
by
  simp [Set.preimage, SetRel.preimage]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
i : M
hi : i ∈ ↑p
j : N
hj : j ∈ ↑q
⊢ (fun m n ↦ (f m) n) i j ∈ ↑(map₂ f p q)

Tactic:
exact apply_mem_map₂ _ hi hj

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun m n ↦ (f.flip m) n) ↑q ↑p) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
Set.image2_swap

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b ↦ (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
by
  suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
⊢ map₂ f s (R ∙ n) = map (f.flip n) s

Tactic:
← map₂_span_singleton_eq_map,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
⊢ map₂ f s (R ∙ n) = map₂ f.flip (R ∙ n) s
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ r.inv.IsWellFounded

Tactic:
IsWellFounded,

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ WellFounded fun x1 x2 ↦ (x1, x2) ∈ r.inv
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 : M ⊗[R] N →ₗ[R] P
⊢ lift ((mk R M N).compr₂ f) = f

Tactic:
by
  rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]

Goal state after:
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
⊢ LinearMap.id ∘ₗ f = f

Tactic:
LinearMap.id_comp

Goal state after:
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
⊢ f = f
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height (RelSeries.last p')
⊢ ↑p.length ≤ height x + 1

Tactic:
simpa [p', hlast'] using! this

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ height x ≤ (↑m + 1) * height (f x) + ↑m

Tactic:
generalize h' : Order.height (f x) = n

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
n : ℕ∞
h' : height (f x) = n
⊢ height x ≤ (↑m + 1) * n + ↑m
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
n : ℕ∞
h' : height (f x) = n
⊢ height x ≤ (↑m + 1) * n + ↑m

Tactic:
cases n with | top => simp | coe n =>
    induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.natCast_lt_top _)).ne
      have h_lt : n' < n := ENat.natCast_lt_natCast.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.natCast_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.natCast_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.natCast_one, ← ENat.natCast_add, ENat.natCast_le_natCast]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.natCast_lt_natCast.mp ((le_add_left le_rfl).trans_lt h_len)
    lia

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure (↑M * ↑N)

Tactic:
← closure_mul_closure,

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure ↑M * closure ↑N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ toSubMulAction 1 ↔ x✝ ∈ 1

Tactic:
rw [one_eq_span, SubMulAction.mem_one]

Goal state after:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ (R ∙ 1).toSubMulAction ↔ ∃ r, r • 1 = x✝
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y

Tactic:
refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hT : T.FG
hST : S ≤ T
⊢ S.FG

Tactic:
rw [← Module.Finite.iff_fg] at hT
  exact FG.of_le_of_isNoetherian hST

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

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

Tactic:
rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
y : S
⊢ f.symm y ∈ I ↔ y ∈ map f I

Tactic:
← comap_symm,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
y : S
⊢ f.symm y ∈ I ↔ y ∈ comap f.symm I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
x : R
⊢ f x ∈ map f I ↔ x ∈ I

Tactic:
← comap_symm,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
x : R
⊢ f x ∈ comap f.symm I ↔ x ∈ I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ 1 • m = 1 • m'
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ y ∈ map f J

Tactic:
← hx.right

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' A
y : S
hy : y ∈ map f (sInf A)
x : R
hx : x ∈ sInf A ∧ f x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ f x ∈ map f J
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
m : Ideal R
inst✝ : m.IsMaximal
hk : RingHom.ker f ≤ m
h : map f m = ⊤
⊢ False

Tactic:
apply congr_arg (comap f) at h

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
m : Ideal R
inst✝ : m.IsMaximal
hk : RingHom.ker f ≤ m
h : comap f (map f m) = comap f ⊤
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
h : I ⊔ J = ⊤
⊢ I ^ n ⊔ J = ⊤

Tactic:
rw [sup_comm, sup_pow_eq_top' (sup_comm I J ▸ h)]

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

Goal state before:
pp: case mp
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : u ∈ span {x}
v : R
hv : v ∈ span {y}
h1 : u + v = 1
⊢ IsCoprime x y

Tactic:
mem_span_singleton'

Goal state after:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y u : R
hu : ∃ a, a * x = u
v : R
hv : ∃ a, a * y = v
h1 : u + v = 1
⊢ IsCoprime x y
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ α

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ?refine_1

pp: case refine_3
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd 0 ?refine_1 = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
· exact gcd {x ∈ s | f x ≠ 0} f

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f)

case refine_3
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize (x * y) = normalize x * normalize y

Tactic:
normalize,

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y * ↑(normUnit (x * y)) = x * ↑(normUnit x) * (y * ↑(normUnit y))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)

Tactic:
by
  simp only [isCoprime_iff_add, one_eq_top] at hf ⊢
  exact sup_iInf_eq_top hf

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
h : normalize b = b
⊢ gcd a b = b ↔ b ∣ a

Tactic:
by simpa only [gcd_comm a b] using gcd_eq_left_iff b a h

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
⊢ IsUnit (gcd (d₁ ^ k) b)

Tactic:
apply isUnit_of_dvd_one

Goal state after:
α : 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₁ ^ k) b ∣ 1
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
⊢ IsUnit (gcd d₁ b)

Tactic:
apply isUnit_of_dvd_one

Goal state after:
α : 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 ∣ 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ (p + q) * r ^ k ∈ m

Tactic:
← hcxq,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ (p + c * x) * r ^ k ∈ m
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal (map f (comap f I))

Tactic:
exact hI.map_ringHom f

Goal state after: