mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B : Finset ((i : ι) → G i)
hA : A.Nonempty
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) →
      x.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ x, UniqueMul A x a0 b0

Tactic:
intro B

Goal state after:
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
⊢ (∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0) → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
inst✝¹ : Semiring R
inst✝ : Finite η
s : Set η
v : η → R
⊢ v ∈ spanSubset R s ↔ ∀ i ∉ s, v i = 0

Tactic:
by
  simp [spanSubset, Module.Basis.mem_span_image, Finsupp.support_subset_iff]

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

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := ⋯
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B : Finset ((i : ι) → G i)
⊢ ∀ (x : Finset ((i : ι) → G i)),
    (∀ y ⊂ x, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2) →
      1 < #A * #x → ∃ p1 ∈ A ×ˢ x, ∃ p2 ∈ A ×ˢ x, p1 ≠ p2 ∧ UniqueMul A x p1.1 p1.2 ∧ UniqueMul A x p2.1 p2.2

Tactic:
intro B

Goal state after:
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
⊢ (∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2) →
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥p
⊢ (p.projectionOnto q h) ↑x = x

Tactic:
simp [projectionOnto, prodEquivOfIsCompl_symm_apply_left]

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
ha₀ : a ≠ 0
⊢ a = 0 → Nonempty ι

Tactic:
simp [ha₀]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsIdempotentElem f
x : M
x✝ : x ∈ f.range
y : M
hy : f y = x
⊢ f x = x

Tactic:
by rw [← hy, ← Module.End.mul_apply, hf.eq]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∃! f, Function.graph f = R) ↔ ∀ (a : α), ∃! b, (a, b) ∈ R

Tactic:
constructor
  · rintro ⟨f, rfl, _⟩ x
    simp
  intro h
  choose f hf using fun x ↦ (h x).exists
  refine ⟨f, ?_, by aesop⟩
  ext ⟨a, b⟩
  constructor
  · aesop
  · exact (h _).unique (hf _)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : 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 : ↑i + 1 < ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun ⟨↑m - 1, ⋯⟩.succ

pp: case e'_4.h
α : 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 : ↑i + 1 < ↑m
⊢ i.succ.castSucc < m.succ

Tactic:
swap

Goal state after:
case e'_4.h
α : 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 : ↑i + 1 < ↑m
⊢ i.succ.castSucc < m.succ

case e'_4
α : 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 : ↑i + 1 < ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun ⟨↑m - 1, ⋯⟩.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : 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 : ↑i + 1 = ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun i.succ

pp: case e'_4.h
α : 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 : ↑i + 1 = ↑m
⊢ i.succ.castSucc < m.succ

Tactic:
swap

Goal state after:
case e'_4.h
α : 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 : ↑i + 1 = ↑m
⊢ i.succ.castSucc < m.succ

case e'_4
α : 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 : ↑i + 1 = ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun i.succ
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a
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 : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) ≤ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
map₂_le

Goal state after:
case a
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 : Set M
t : Set N
⊢ ∀ m ∈ span R s, ∀ n ∈ span R t, (f m) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ ↑n ≤ height x

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
cases hn : n with
    | zero => simp
    | succ => simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
        coe_lt_height_iff, *]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim (↑(Set.Ici x))ᵒᵈ

Tactic:
Order.krullDim_eq_of_orderIso (OrderIso.refl _)

Goal state after:
α : Type u_3
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim (↑(Set.Ici x))ᵒᵈ
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 : α
⊢ coheight x ≤ (↑m + 1) * coheight (f x) + ↑m

Tactic:
by
  rw [Order.coheight, Order.coheight]
  apply height_le_of_krullDim_preimage_le (f := f.dual)
  exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {x})) (h x)

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
← one_mul a∗

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ 1 * a∗ ≤ 1 + a∗ * a
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
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • x * y ∈ I

Tactic:
rw [Algebra.smul_mul_assoc]

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
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I
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

Goal state after:
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 : Module.Finite R ↥T
hST : S ≤ T
⊢ S.FG
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⇑(algebraMap R S) '' ↑I • N) = ↑I • Submodule.restrictScalars R N

Tactic:
Submodule.set_smul_eq_iSup,

Goal state after:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ a ∈ ⇑(algebraMap R S) '' ↑I, a • N) = ⨆ a ∈ ↑I, a • Submodule.restrictScalars R N
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:
← I.span_eq

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : (Ideal.span ↑I).IsTwoSided
s : Set M
x : M
⊢ x ∈ Ideal.span ↑I • span R s ↔ x ∈ span R (↑(Ideal.span ↑I) • s)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
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
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x

pp: case mpr
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
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)

Tactic:
swap

Goal state after:
case mpr
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
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x) → x ∈ I • span R (Set.range f)

case mp
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
f : ι → M
x : M
⊢ x ∈ I • span R (Set.range f) → ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = x
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = b✝ - (a * s + b * t) * (b✝ / a✝)

Tactic:
← p,

Goal state after:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = b✝ - a✝ * (b✝ / a✝)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y = z ↔ x = y * z

Tactic:
by
  obtain ⟨a, ha⟩ := h2
  rw [ha, mul_div_cancel_left₀ _ h1]
  simp only [mul_eq_mul_left_iff, h1, or_false]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
swap

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
swap

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
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
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : ∃ x ∈ I, f x = f (a * b)
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
rcases hxy with ⟨c, hc, hc'⟩

Goal state after:
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
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f c = f (a * b)
⊢ x ∈ map f I ∨ y ∈ map f 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
x y : B
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)

Tactic:
simp only [hf _]

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

Goal state before:
pp: case pos
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : x✝ = 1
⊢ Associates.mk 1 = x✝

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
x✝ : Associates α
h : ¬x✝ = 1
⊢ Associates.mk (Quotient.out x✝) = x✝

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : ¬gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
· induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
h : f = 0
⊢ IsUnit (f.prod * ↑u)

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α

Tactic:
by
  have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h
  constructor
  convert! InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this
  ext
  exact Ideal.span_singleton_lt_span_singleton.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
⊢ Prime x

Tactic:
have ane0 := ne_zero_of_mem_factors hx

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
ane0 : a ≠ 0
⊢ Prime x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ I * J ≤ P ↔ I ≤ P ∨ J ≤ P

Tactic:
by
  rw [or_comm, Ideal.mul_le]
  simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
by_cases h : a = 0 ∨ b = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (ℕ →₀ R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ Injective ⇑(Finsupp.lmapDomain R R Fin.val ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R (Fin (n + 1))).symm)

Tactic:
simpa using! Finsupp.mapDomain_injective Fin.val_injective

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsCoprime (Ideal.span {x}) (Ideal.span {y})

Tactic:
Ideal.isCoprime_iff_sup_eq,

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ Ideal.span {x} ⊔ Ideal.span {y} = ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
split_ifs with h h_1
      · rw [h]
        apply dvd_zero
      · exact (normalize_associated _).dvd
      have h0 : lcm a b ≠ 0 := lcm_ne_zero_iff.mpr ⟨h, h_1⟩
      rw [normalize_dvd_iff, ← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_comm, mul_dvd_mul_iff_right h]
      apply dvd_lcm_right

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M N : Matrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : P
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : ¬P
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

Tactic:
simp [h]

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

Goal state before:
pp: case pos
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
simp [h]

Goal state after: