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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
simpa [hq] using hp hx

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case h
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
⊢ φ = Pi.evalAlgHom k (fun i ↦ k) s

Tactic:
refine AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)

Goal state after:
case h
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
h3 : φ (Pi.single s 1) = 1
t : G
⊢ φ.toLinearMap ((Pi.basisFun k G) t) = (Pi.evalAlgHom k (fun i ↦ k) s).toLinearMap ((Pi.basisFun k G) t)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∃ l_1 ∈ supported R R (g '' ↑t1), (linearCombination R id) l_1 = (linearCombination R id).toFun ((lmapDomain R R g) l)

Tactic:
refine ⟨_, ?_, rfl⟩

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (lmapDomain R R g) l ∈ supported R R (g '' ↑t1)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : M × P
e : f x.1 + ↑l x.2 = f y.1 + ↑l y.2
this : x.2 = y.2
⊢ f x.1 = f y.1

Tactic:
rwa [this, add_left_inj] at e

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ comap T f.ker

Tactic:
Module.End.mem_invtSubmodule

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ≤ comap T f.ker ↔ f.ker ≤ comap T f.ker
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    (f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.range ≤ map (↑((GeneralLinearGroup.generalLinearEquiv R E) T)) f.range) ∧
      f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.ker ≤ map (↑((GeneralLinearGroup.generalLinearEquiv R E) T)) f.ker

Tactic:
← Module.End.mem_invtSubmodule_symm_iff_le_map,

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    (f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm) ∧
      f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
s : RelSeries r
x : α
p : RelSeries r
i : ℕ
hi : i < p.toList.length
⊢ i < p.length + 1

Tactic:
simpa using hi

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

Goal state before:
pp: case refine_3
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ ↑↑e ∘ₗ f = LinearMap.id

Tactic:
(LinearEquiv.eq_toLinearMap_symm_comp _ _).mp e.2.1

Goal state after:
case refine_3
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ inl R M P = LinearMap.id
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
⊢ height a = height (f a)

Tactic:
by
  have : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a)) :=
    coheight_eq_of_strictMono (α := αᵒᵈ) (β := βᵒᵈ) (f := OrderDual.toDual ∘ f ∘ OrderDual.toDual)
    (strictMono_dual_iff.mp hf) (fun a b hab ↦ h a b hab) _
  simpa [Order.coheight_toDual] using this

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = 0 ↔ IsMin x

Tactic:
simpa [isMin_iff_forall_not_lt] using height_le_coe_iff (x := x) (n := 0)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b

pp: case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ ?b < ⊤

pp: case b
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ WithTop α

Tactic:
· exact p.monotone (Fin.le_last _)

Goal state after:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤
Module: Mathlib.Algebra.Module.Submodule.Finsupp

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

Tactic:
rw [AddSubmonoid.coe_finsetSum]

Goal state after:
case le
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)
⊢ ∑ i ∈ c.support, ↑((DistribSMul.toLinearMap R (↥N) i) (c i)) ∈ sR • N
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x y : A),
    x ∈ closure (↑N ∪ ↑P) →
      y ∈ closure (↑N ∪ ↑P) → m • x ∈ M • N ⊔ M • P → m • y ∈ M • N ⊔ M • P → m • (x + y) ∈ M • N ⊔ M • P

Tactic:
intro _ _ _ _ h1 h2

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • (x✝ + y✝) ∈ M • N ⊔ M • P
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := ⋯
sli : List α := ⋯
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
⊢ ↑hi.choose ≠ ↑hj.choose

Tactic:
contrapose h_eq

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hi.choose ≤ ↑hj.choose
h_eq : ↑hi.choose = ↑hj.choose
⊢ sli[↑hi.choose] = sli[↑hj.choose]
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 : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
by
  obtain rfl | hn := Decidable.eq_or_ne n 0
  · rw [Submodule.pow_zero, pow_zero]
    exact le_one_toAddSubmonoid
  · exact (pow_toAddSubmonoid M hn).ge

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
M✝¹ : Type u_1
inst✝⁵ : AddCommMonoid M✝¹
inst✝⁴ : Module R M✝¹
inst✝³ : Module A M✝¹
inst✝² : IsScalarTower R A M✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ M = 0

Tactic:
by
    rw [Submodule.zero_eq_bot, Submodule.eq_bot_iff]
    rintro m hm
    obtain ⟨n, hn⟩ := hM
    exact eq_zero_of_pow_eq_zero <| (M ^ n).eq_bot_iff.mp hn _ (pow_mem_pow M hm n)

Goal state after:
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 t : Submodule R A
⊢ s * t = span R (↑s * ↑t)

Tactic:
by
  rw [mul_eq_map₂]; exact map₂_eq_span_image2 _ s t

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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx : x ∈ M ^ 0
⊢ C 0 x hx

Tactic:
rw [pow_zero] at hx

Goal state after:
case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx✝ : x ∈ M ^ 0
hx : x ∈ 1
⊢ C 0 x hx✝
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx : x ∈ M ^ 0
⊢ C 0 x hx

Tactic:
rw [pow_zero] at hx

Goal state after:
case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx✝ : x ∈ M ^ 0
hx : x ∈ 1
⊢ C 0 x hx✝
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 = a * b / a

Tactic:
mul_div_cancel_left₀ _ ha

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

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * (b * d) / a = b * d

Tactic:
mul_div_cancel_left₀ _ ha

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b * d = b * d
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a

Tactic:
rw [gcd]
  split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : EuclideanDomain R
n : ℕ
c : R
⊢ (0 * c / 0) ^ n = (0 * c) ^ n / 0 ^ n

pp: case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
· obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Goal state after:
case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M) (b : M'), (x✝ • a, x✝ • b) = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0

Tactic:
Prod.mk_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ (∀ (a : M) (b : M'), x✝ • a = 0 ∧ x✝ • b = 0) ↔ (∀ (m : M), x✝ • m = 0) ∧ ∀ (m : M'), x✝ • m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ (I ^ Nat.zero).IsTwoSided

Tactic:
rw [Submodule.pow_zero, one_eq_top]; infer_instance

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y + z / t = (t * x + y * z) / (t * y)

Tactic:
apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
  rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ (x : α), x ∈ s → x = 0

Tactic:
intro h x hx

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ x = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
classical
    by_cases! h : ∀ x ∈ s, x = (0 : α)
    · use replicate (card s) 1
      rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton,
    ← gcd_dedup, dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
      exact ⟨⟨rfl, h⟩, normalize_one⟩
    · choose f hf using @gcd_dvd _ _ _ s
      refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
      · rw [map_pmap]
        conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
        congr with (x hx)
        rw [id, ← hf hx]

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

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

Tactic:
rw [filter_insert]

Goal state after:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
simp only [gcd_zero_left, normalize_gcd]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
rw [← isCoprime_iff_codisjoint, ← isCoprime_iff_add, ← isCoprime_iff_exists,
      ← isCoprime_iff_sup_eq]
  simp

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ a * b = d₁ ^ k * d₂ ^ k

Tactic:
rw [h, hc]

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P

Tactic:
hp.multiset_prod_le,

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ (∃ I ∈ Multiset.map f s, I ≤ P) ↔ ∃ i ∈ s, f i ≤ P
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ S = ⊥ ↔ generator S = 0

Tactic:
← @span_singleton_eq_bot R M,

Goal state after:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ S = ⊥ ↔ R ∙ generator S = ⊥
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
mul_comm a,

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) * a ∣ c * (d * a)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
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 : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)

Tactic:
rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_right_comm (f a : Set R),
          Set.union_eq_self_of_subset_left Ha] at h

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 : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ x ∈ ↑t, ↑(f x)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
⊢ ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y

Tactic:
mul_comm a,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = x * a + b * y