mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n = lift.{v, u} o ↔ ω_ ↑n = o

Tactic:
simpa using lift_inj (a := ω_ n)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ i, f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
by
  rw [lift_iSup bddAbove_of_small] at h
  apply (lift_iSup_le_sum f).antisymm'
  convert! sum_le_lift_mk_mul_iSup_lift f
  rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h,
    lift_iSup bddAbove_of_small]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
exact extend_function_finite f h

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑s < lift.{u_1, u_2} #β

Tactic:
← h,

Goal state after:
case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑s < lift.{u_2, u_1} #α
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
i : ι
⊢ i ∈ f.support ↔ f i ≠ 0

Tactic:
simp only [DFinsupp.mem_support_iff]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ (extendWith x 0) none = (single none x) none

pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Tactic:
· rw [extendWith_none, single_eq_same]

Goal state after:
case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f) ↔
    x ∈ AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i))

Tactic:
simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]

Goal state after:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f) ↔ ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x) → ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
rintro ⟨f, hf, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ ∃ f_1, (f_1.sum fun x xi ↦ ↑xi) = f.sum fun _i xi ↦ xi
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
f : M → N
g : N → O
⊢ mapDomainLinearMap R S (g ∘ f) = mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f

Tactic:
ext; simp [Finsupp.mapDomain_comp]

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
f : N →ₙ* O
g : M →ₙ* N
⊢ mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)

Tactic:
ext; simp [Finsupp.mapDomain_comp]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
by_cases h : Disjoint (image (f a) t) (image₂ f s t)

Goal state after:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : ¬Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)
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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : u.card = (insert b₂ s' ∪ t).card
⊢ u.card = (s' ∪ insert b₁ t).card

Tactic:
simp [eq, hb₂t', hb₁t, hb₁s']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
⊢ 0 < #s

Tactic:
by rwa [length_sort] at h

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

Goal state before:
pp: G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b2
this : b1 ∈ {b1, b2}
⊢ b1 = b2

Tactic:
obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩

Goal state after:
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a✝ b1 b2 : G
he : (fun x ↦ a✝ * x) b1 = (fun x ↦ a✝ * x) b2
this : b1 ∈ {b1, b2}
a : G
ha : a ∈ {a✝}
b : G
hb : b ∈ {b1, b2}
hu : UniqueMul {a✝} {b1, b2} a b
⊢ b1 = b2
Module: Mathlib.LinearAlgebra.Finsupp.Span

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

Tactic:
rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)

Goal state after:
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
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : R ∙ m ≤ ⨆ i, p i → ∃ s, R ∙ m ≤ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i

Tactic:
simp only [Submodule.span_singleton_le_iff_mem] at this

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : m ∈ ⨆ i, p i
this : m ∈ ⨆ i, p i → ∃ s, m ∈ ⨆ i ∈ s, p i
⊢ ∃ s, m ∈ ⨆ i ∈ s, p i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ (if 1 = n then 1 else 0) = 0

Tactic:
if_neg hn.symm

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).toFinsupp = single n a

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ 1 • p = 0

Tactic:
← h,

Goal state after:
R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ 0 • p = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (single n a).coeff.support ⊆ {n}

Tactic:
exact Finsupp.support_single_subset

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
rw [X, H, monomial_zero_right, support_zero]

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

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), ¬a < f x
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
not_lt

Goal state after:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (q.toFun ⟨↑i - (p.length + 1), ⋯⟩, q.toFun ⟨↑i - p.length, ⋯⟩) ∈ r

Tactic:
convert! q.step ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <| by lia⟩

Goal state after:
case e'_4.e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ ↑i - p.length = ↑⟨↑i - (p.length + 1), ⋯⟩.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case length_eq
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ ((p.append q hpq).append w ⋯).length = (p.append (q.append w hqw) ⋯).length

Tactic:
simp only [append_length, Nat.add_left_inj]
    lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m = ↑i
⊢ ↑m + 1 = ↑i + 1

Tactic:
rw [hm]

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' : RelSeries {(a, b) | a < b} := (RelSeries.eraseLast p).snoc a ⋯
⊢ p.length = p'.length

Tactic:
simp [p']; lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

Tactic:
rw [height_le_iff]

Goal state after:
case mp
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n) → ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ 0 ≤ krullDim α ↔ Nonempty α

Tactic:
by
  contrapose!
  rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ ¬krullDim α < 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder] at h
    cases h

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

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
a : α
⊢ a ∈ ∏ i ∈ ∅, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ ∅ → g i ∈ f i), ∏ i ∈ ∅, g i = a

Tactic:
simp_rw [Finset.prod_empty, Set.mem_one]
      exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.notMem_empty _ hi), h.symm⟩,
        fun ⟨_, _, hf⟩ ↦ hf.symm⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p : Submodule R P
q : Submodule R Q
⊢ (mapIncl p q).range = Submodule.map₂ (mk R P Q) p q

Tactic:
mapIncl,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
P : Type u_9
Q : Type u_10
inst✝³ : AddCommMonoid P
inst✝² : AddCommMonoid Q
inst✝¹ : Module R P
inst✝ : Module R Q
p : Submodule R P
q : Submodule R Q
⊢ (map p.subtype q.subtype).range = Submodule.map₂ (mk R P Q) p q
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : n ≠ 0
⊢ ↑n = 1

Tactic:
← Nat.one_le_iff_ne_zero

Goal state after:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
⊢ ↑n = 1
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a * a = a

Tactic:
← h,

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a∗ * a∗ = a∗
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:
rw [pow_zero, pow_zero]
    exact subset_coe_one

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * 1

Tactic:
← h,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x + b * y)
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 + y * z) y

Tactic:
exact h.add_mul_left_left z

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsCoprime (x + 1) (x - 1)

Tactic:
by
  simpa [show 2 + (x - 1) = x + 1 by ring] using add_mul_left_left (sub_one_right_of_dvd h) 1

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
h : 2 ∣ x
⊢ IsRelPrime (x + 1) (x - 1)

Tactic:
by
  simpa [show 2 + (x - 1) = x + 1 by ring] using add_mul_left_left (sub_one_right_of_dvd h) 1

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
N P : Submodule R A
h : N * P = 1
| 1 * ⊤

Tactic:
← h,

Goal state after:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
| N * P * ⊤
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
N P : Submodule R A
h : N * P = 1
| ⊤ * 1

Tactic:
← h,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
N P : Submodule R A
h : N * P = 1
| ⊤ * (N * P)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ (↑((↑span.ringHom).comp SetSemiring.singletonMonoidHom)).toFun 0 = 0

Tactic:
simp [SetSemiring.singletonMonoidHom]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommGroup M
a : M
⊢ (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a

Tactic:
by
  ext i
  simp [Submodule.mem_span_singleton, AddSubgroup.mem_zmultiples_iff]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a % b ↔ c ∣ a

Tactic:
by
  rw [← dvd_add_right (h.mul_right _), div_add_mod]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b

Tactic:
← h,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = a * b / b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = c / a

Tactic:
← h,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = a * b / a
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, q.IsPrime ∧ comap f q = p

Tactic:
obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)
    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.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n

Tactic:
by
  induction n with
  | zero => rw [Submodule.pow_zero, Submodule.pow_zero]
  | succ _ hn =>
    rw [Submodule.pow_succ, Submodule.pow_succ]
    exact Ideal.mul_mono hn e

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ span (⇑f '' {r}) * map f I = f r • map f I

Tactic:
Set.image_singleton,

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ span {f r} * map f I = f r • map f I
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
⊢ Associated |a * b| (a * b)

Tactic:
abs_eq_normalize

Goal state after:
a b : ℤ
⊢ Associated (normalize (a * b)) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case h
a : ℤ
h : a = ↑a.natAbs
⊢ ↑a.natAbs = 1 * a

Tactic:
← h,

Goal state after:
case h
a : ℤ
h : a = ↑a.natAbs
⊢ a = 1 * a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ (↑Finset.univ).Pairwise (Function.onFun IsCoprime I)

Tactic:
Finset.coe_univ,

Goal state after:
case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Set.univ.Pairwise (Function.onFun IsCoprime I)
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
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
← hh

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
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
    · rw [filter_union_filter_not_eq]
    rw [gcd_union]
    refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
    · exact gcd {x ∈ s | f x ≠ 0} f
    · refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
      · simp
      · intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]
    simp only [gcd_zero_left, normalize_gcd]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ Ideal.span (⇑f '' {x}) = Submodule.span S (⇑f '' {x})

Tactic:
Set.image_singleton,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ Ideal.span {f x} = S ∙ f x
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
a : Associates α
⊢ α

Tactic:
by classical exact if a = 1 then 1 else a.out

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b c : α
⊢ Associated (gcd (0 * b) (0 * c)) (0 * gcd b c)

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ ∃ d, Associated (d ^ k) a

Tactic:
use 1
    rw [one_pow]
    apply (associated_one_iff_isUnit.mpr hab).symm.trans
    rw [hb]
    exact gcd_zero_right' a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ IsPrimal a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ IsPrimal 0

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a