mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x y : B
⊢ g x + g y = g (f (g x)) + g (f (g y))

Tactic:
h₂,

Goal state after:
R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x y : B
⊢ g x + g y = g x + g (f (g y))
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length

Tactic:
exact heq

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
p : RelSeries r
this : {n : ℕ} → p.length = n → motive p :=
  fun {n} heq ↦
    Nat.recAux (motive := fun {n} ↦ (p : RelSeries r) → p.length = n → motive p) (fun p heq ↦ ⋯.mpr (singleton p.head))
      (fun d hd p heq ↦
        have lq := ⋯;
        ⋯.mpr (cons (p.tail ⋯) p.head ⋯ (hd (p.tail ⋯) ⋯)))
      n p heq
⊢ motive p

Tactic:
exact this rfl

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ p.length ≠ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
⊢ p.length = (RelSeries.singleton r p.head).length

Tactic:
exact heq

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
this : {n : ℕ} → p.length = n → motive p :=
  fun {n} heq ↦
    Nat.recAux (motive := fun {n} ↦ (p : RelSeries r) → p.length = n → motive p) (fun p heq ↦ ⋯.mpr (singleton p.head))
      (fun d hd p heq ↦
        have ne0 := ⋯;
        have len := ⋯;
        ⋯.mpr (snoc p.eraseLast p.last ⋯ (hd p.eraseLast len)))
      n p heq
⊢ motive p

Tactic:
exact this rfl

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
⊢ ∀ (i : Fin (p.length + q.length)),
    (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun i.castSucc, Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun i.succ) ∈ r

Tactic:
apply Fin.addCases <;> intro i

Goal state after:
case left
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd q.length i).succ) ∈
    r

case right
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin q.length
⊢ (Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).castSucc,
      Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length i).succ) ∈
    r
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ ↑n < height x ∧ height x ≤ ↑n + 1

Tactic:
le_antisymm_iff,

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ∧ ↑n + 1 ≤ height x ↔ ↑n < height x ∧ height x ≤ ↑n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
hh : height a = ⊤
⊢ ⊤ + coheight a ≤ ⨆ p, ↑p.length

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
hch : coheight a = ⊤
⊢ ↑n + ⊤ ≤ ⨆ p, ↑p.length

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: n : ℕ∞
⊢ height n = n

Tactic:
cases n with
  | top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
  | coe n => exact (height_coe_withTop _).trans (height_nat _)

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

Goal state before:
pp: case le.refine_2.mpr
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
x : M
⊢ x ∈ sR • N → sR • N ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p} → x ∈ sR • N

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + l

Tactic:
h₂,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + 0
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map (map f g) ⊤ = Submodule.map₂ ((mk R P Q).compl₁₂ f g) ⊤ ⊤

Tactic:
← map₂_mk_top_top_eq_top,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map (map f g) (Submodule.map₂ (mk R M N) ⊤ ⊤) = Submodule.map₂ ((mk R P Q).compl₁₂ f g) ⊤ ⊤
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1

Tactic:
by rwa [smul_mul_assoc, ← mul_smul_comm]

Goal state after:
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
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ M ^ (n + 1) = M * M ^ n

Tactic:
by
  rw [add_comm, M.pow_add h, Submodule.pow_one]

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

Goal state before:
pp: case e'_2
R : Type u
I : Type v
inst✝³ : CommSemiring R
s : I → R
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]

Goal state after:
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:
HSMul.hSMul,

Goal state after:
ι : 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
⊢ span R (SetSemiring.down (s * t)) * P = span R (SetSemiring.down s) * (span R (SetSemiring.down t) * P)
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
P : Submodule R A
⊢ 1 • P = P

Tactic:
HSMul.hSMul,

Goal state after:
ι : 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
P : Submodule R A
⊢ span R (SetSemiring.down 1) * P = P
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 • P + t • P

Tactic:
HSMul.hSMul,

Goal state after:
ι : 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
⊢ span R (SetSemiring.down (s + t)) * P = span R (SetSemiring.down s) * P + span R (SetSemiring.down t) * P
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
P : Submodule R A
⊢ 0 • P = 0

Tactic:
HSMul.hSMul,

Goal state after:
ι : 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
P : Submodule R A
⊢ span R (SetSemiring.down 0) * P = 0
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : A
hx : ∀ y ∈ J, x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1 ∈ I, h y_1 = h x * h y

Tactic:
exact ⟨x * y, hx _ hy, map_mul h x y⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
x✝ : R ∙ v i = ⊥
⊢ v i = 0

Tactic:
simp_all

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

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊥

Tactic:
· apply w
      exact Nat.succ_le_succ_iff.mp p

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ x ∈ M'

Tactic:
suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
    rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)
  rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]
  exact fun r hr ↦ H ⟨r, hr⟩

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0

Tactic:
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd a 0 = a

Tactic:
rw [gcd]
  split_ifs with h <;> simp only [h, zero_mod, gcd_zero_left]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
q : Ideal S
hq₁ : q.IsPrime
hq₂ : map f p ≤ q
hq₃ : Disjoint ↑q ↑(Submonoid.map f p.primeCompl)
⊢ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩

Goal state after:
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
ι : Sort w
f : ι → Submodule R M
r : R
H : r ∈ ⨅ i, (f i).annihilator
n : M
hn : n ∈ ⨆ i, f i
m₁ m₂ : M
h₁ : r • m₁ = 0
h₂ : r • m₂ = 0
⊢ 0 + r • m₂ = 0

Tactic:
h₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort w
f : ι → Submodule R M
r : R
H : r ∈ ⨅ i, (f i).annihilator
n : M
hn : n ∈ ⨆ i, f i
m₁ m₂ : M
h₁ : r • m₁ = 0
h₂ : r • m₂ = 0
⊢ 0 + 0 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
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
⊢ sInf (map f '' A) ≤ map f (sInf A)

Tactic:
intro y hy
    obtain ⟨x, hx⟩ := hf y
    refine hx ▸ mem_map_of_mem f ?_
    have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
    rw [Submodule.mem_sInf]
    intro J hJ
    rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
    have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
    simpa only [sub_add_cancel] using J.add_mem this hx'

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : n ≠ 0 → ↑n = ⊤
hn : n + 1 ≠ 0
⊢ ↑(n + 1) = ⊤

Tactic:
obtain rfl | n := n; · rw [Nat.cast_one, one_eq_top]
    rw [Nat.cast_succ, ih n.succ_ne_zero, add_eq_sup, top_sup_eq]

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

Goal state before:
pp: a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b

Tactic:
rw [Int.associated_iff_natAbs]

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ f x * a) = s.gcd f * normalize a

Tactic:
simp_rw [mul_comm]

Goal state after:
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ f x * a) (s.gcd f * a)

Tactic:
simp_rw [mul_comm]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ (if a = 0 then 1 else Exists.choose ⋯) = u⁻¹ * if a = 0 then 1 else Exists.choose ⋯

Tactic:
if_neg ha,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ Exists.choose ⋯ = u⁻¹ * Exists.choose ⋯
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
h : Associated a b
ha : normalize a = a
hb : normalize b = b
⊢ a = b

Tactic:
rw [← ha, normalize_eq_normalize_iff_associated.mpr h, hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
ha : a ≠ 0
⊢ gcd a b ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
ha : a ≠ 0
⊢ gcd a b ≠ 0

Tactic:
by
  simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hb : b ≠ 0
⊢ gcd a b ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hb : b ≠ 0
⊢ gcd a b ≠ 0

Tactic:
by
  simp_all

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical = I ↔ I.IsRadical

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical ≤ I ∧ I ≤ I.radical ↔ I.IsRadical
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
⊢ 1 * ↑(Units.mkOfMulEqOne a b h) = a

Tactic:
rw [Units.val_mkOfMulEqOne, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
hx : Irreducible x
⊢ IsUnit (gcd x y) ↔ ¬x ∣ y

Tactic:
rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]

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

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑∅, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i

Tactic:
rw [Finset.coe_empty, Set.biUnion_empty, Set.union_empty, subset_union] at h

Goal state after:
case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : I ≤ f a ∨ I ≤ f b
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Classical.choose ⋯ = (if a = 0 then 1 else Classical.choose ⋯) * if b = 0 then 1 else Classical.choose ⋯

Tactic:
if_neg ha,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Classical.choose ⋯ = Classical.choose ⋯ * if b = 0 then 1 else Classical.choose ⋯
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
⊢ ∀ k ∈ insert i u, (f k).IsPrime

Tactic:
rw [Finset.forall_mem_insert] at hp ⊢

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ (f j).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime
hjt : j ∈ insert j u
⊢ (f i).IsPrime ∧ ∀ x ∈ u, (f x).IsPrime
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b c : G₀
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ if c = 0 ∧ b = 0 then 0 else 1

Tactic:
simp_all

Goal state after: