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

Goal state before:
pp: case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ (c • 1) • a • x + (-a • 1) • c • x = 0

Tactic:
simp only [smul_assoc, one_smul, neg_smul]

Goal state after:
case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ c • a • x + -(a • c • x) = 0
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
a : V
h : LinearIndepOn K id s
⊢ a ∈ span K s ↔ LinearIndepOn K id (insert a s) → a ∈ s

Tactic:
simpa using h.mem_span_iff (a := a)

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ ↑(image₂ f (s ∩ s') t) = ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
push_cast
    exact image2_inter_left hf

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ (mapDomain f (comapDomain f hf x)).coeff = x.coeff

Tactic:
exact Finsupp.mapDomain_comapDomain _ hf _ hx

Goal state after:
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
⊢ ↑({x ∈ t | x ∈ s}) ⊆ s

Tactic:
by simp [Set.subset_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
motive : R[M] → Prop
x : R[M]
zero : motive 0
single_add : ∀ (m : M) (r : R) (x : R[M]), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)
⊢ motive (ofCoeff 0)

Tactic:
by simpa using zero

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

Goal state before:
pp: R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ ∏ i ∈ cons i s hi, single (m i) (r i) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)

Tactic:
by
    rw [prod_cons, ih, single_mul_single, prod_cons, prod_cons]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑1 = ↑s ^ 0

Tactic:
pow_zero,

Goal state after:
case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ↑1 = 1
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] = s.max' H

Tactic:
by
  let l := s.sort
  apply le_antisymm
  · have : l.get ⟨s.sort.length - 1, h⟩ ∈ s :=
      (s.mem_sort (· ≤ ·)).1 (List.get_mem l _)
    exact s.le_max' _ this
  · have : s.max' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.max'_mem H)
    obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this
    rw [← hi]
    exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.le_sub_one_of_lt i.prop)

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
rintro ⟨a, rfl, ha⟩

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
sSup_eq_iSup,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ ⨆ a ∈ S, a ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a * X ^ 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a * 1)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
a : R
⊢ motive (Polynomial.C a * X ^ 0)

Tactic:
rw [pow_zero, mul_one]; exact C a

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
sSup_eq_iSup,

Goal state after:
s : Set ℕ∞
a : ℕ∞
⊢ a * ⨆ a ∈ s, a = ⨆ b ∈ s, a * b
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ⨅ i, a * f i ≤ a * ⨅ i, f i

Tactic:
← hb,

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ⨅ i, a * f i ≤ a * f b
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
sSup_eq_iSup,

Goal state after:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
sSup_eq_iSup,

Goal state after:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
sSup_eq_iSup,

Goal state after:
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • ⨆ a ∈ s, a = ⨆ a ∈ s, c • a
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
⊢ (fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x) = x

Tactic:
refine Subtype.ext (List.ext_get ?_ fun n hn1 _ => by dsimp; apply List.get_ofFn)

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
x : ↑{x | x ≠ [] ∧ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x}
⊢ (↑((fun x ↦ ⟨x.toList, ⋯⟩) ((fun x ↦ fromListIsChain ↑x ⋯ ⋯) x))).length = (↑x).length
Module: Mathlib.Order.RelSeries

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

Tactic:
push Not

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.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
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), (mk (↑lf) f ⋯).toFun i = (mk (↑lf) g ⋯).toFun i
⊢ f = g

Tactic:
simp_rw [mk_toFun lf f mf, mk_toFun lf g mg, mk_length lf f mf] at feq

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 (↑lf + 1)), f i = g i
⊢ f = g
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, ∀ y ∈ Set.range fun x_2 ↦ (↑x_2).length, y ≤ x_1

Tactic:
push Not

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

Goal state before:
pp: α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
krullDim_eq_iSup_length,

Goal state after:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ ↑(⨆ p, ↑p.length)
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ mulLeft R a ^ 0 = mulLeft R (a ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ 1 = mulLeft R (a ^ 0)
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ 1 = mulLeft R (a ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ 1 = mulLeft R 1
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ mulRight R a ^ 0 = mulRight R (a ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ 1 = mulRight R (a ^ 0)
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ 1 = mulRight R (a ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ 1 = mulRight R 1
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_1
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)
⊢ ∀ c_1 ∈ c.support, ↑((DistribSMul.toLinearMap R (↥N) c_1) (c c_1)) ∈ sR • N

Tactic:
rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (List.map g t).prod ∈ (List.map f t).prod

Tactic:
induction t with

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (List.map f₁ t).prod ⊆ (List.map f₂ t).prod

Tactic:
induction t with

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ x + y
⊢ r • m ∈ s • x + s • y

Tactic:
rw [add_eq_sup, Submodule.mem_sup] at hm

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m
⊢ r • m ∈ s • x + s • y
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid N₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R N₂
inst✝ : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range

Tactic:
exact Submodule.map₂_le_map₂ hab hcd

Goal state after:
Module: Mathlib.Data.Set.Semiring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ up 1 = 1

Tactic:
up_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ lTensor M (f - g) = lTensor M f - lTensor M g

Tactic:
by
  simp_rw [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ ↑p ^ 0 ⊆ ↑(p ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑(p ^ 0)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ closure s ^ 0 = closure (s ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ 1 = closure (s ^ 0)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ 1 = closure (s ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ 1 = closure 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
x y : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0

Tactic:
rintro rfl rfl

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
by
  rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f a * f x + f b * f y = 1

Tactic:
← f.map_mul,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f (a * x) + f b * f y = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f (a * x) + f b * f y = 1

Tactic:
← f.map_mul,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f (a * x) + f (b * y) = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y

Tactic:
exact h.add_mul_right_left z

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

Goal state before:
pp: case succ.zero
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
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ toAddSubmonoid 1 * M.toAddSubmonoid = M.toAddSubmonoid ^ 0 * M.toAddSubmonoid

Tactic:
pow_zero,

Goal state after:
case succ.zero
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
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ toAddSubmonoid 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ R ∙ 1 = (Algebra.linearMap R A).range

Tactic:
LinearMap.span_singleton_eq_range,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (LinearMap.toSpanSingleton R A 1).range = (Algebra.linearMap R A).range
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ 1 = span R (s ^ 0)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ 1 = span R (s ^ 0)

Tactic:
pow_zero,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ 1 = span R 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : Aˣ
⊢ x✝ ∈ (Units.map ↑(spanSingleton R)).ker ↔ x✝ ∈ (Units.map ↑(algebraMap R A)).range

Tactic:
simpa [Units.ext_iff, eq_comm] using span_singleton_eq_one_iff

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

Goal state before:
pp: case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i ↦ s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsRelPrime (s i) (s j)

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
    obtain ⟨hj, ji⟩ := hj
    exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
⊢ ⇑(RingHom.fst R S) '' s ×ˢ t ⊆ s

Tactic:
exact Set.fst_image_prod_subset _ _

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

Goal state before:
pp: case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬⊤.IsPrime

Tactic:
isPrime_iff

Goal state after:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
F : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : FunLike F R S
inst✝¹ : RingHomClass F R S
f : F
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
le : comap f I ≤ P
x✝ : S
⊢ x✝ ∈ ↑I → x✝ ∉ ↑(Submonoid.map f P.primeCompl)

Tactic:
rintro hI ⟨r, hp, rfl⟩; exact hp (le hI)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
hnb : b ≠ 0
⊢ a - a * b / b = 0 ∧ b ≠ 0

Tactic:
by simp [hnb]

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

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

Tactic:
rw [← h]
    apply gcd_dvd_right

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
I : Ideal R
inst✝ : I.IsTwoSided
s : Set M
x : M
⊢ x ∈ I • span R s ↔ x ∈ span R (↑I • s)

Tactic:
by
  rw [← I.span_eq] at *
  rw [Submodule.span_smul_span, I.span_eq]

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

Goal state before:
pp: case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K ^ 0 ≤ comap f (K ^ 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ 1 ≤ comap f (K ^ 0)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ 1 ≤ comap f (K ^ 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ 1 ≤ comap f 1
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
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
⊢ x ∈ I • span R (f '' s) ↔ x ∈ I • span R (Set.range fun i ↦ f ↑i)

Tactic:
← Set.image_eq_range

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
s : Set ι
f : ι → M
x : M
⊢ x ∈ I • span R (f '' s) ↔ x ∈ I • span R (f '' s)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0

Tactic:
· rw [hy, lcm_zero_right]

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

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)

Tactic:
mul_div_cancel_left₀ _ hc0,

Goal state after:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)