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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ LinearIndependent (ι := ↑s) K (v ∘ Subtype.val)

Tactic:
· rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']]
    apply hli.comp
    rintro ⟨i, x, rfl⟩ ⟨j, y, rfl⟩ hij
    simp only [Subtype.ext_iff, hf, f'] at hij
    simp [hij]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r : R
m : M
⊢ single m r = 0 ↔ r = 0

Tactic:
simp [← coeff_inj]

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).sort r = a :: s.sort r

Tactic:
by
  rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
a : α
n : ℕ
⊢ {a} ^ (n + 1) = {a ^ (n + 1)}

Tactic:
simp [pow_succ, singleton_pow _ n]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
⊢ #(∅ ^ m) ≤ #(∅ ^ n)

pp: case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)

Tactic:
· simp [hm]

Goal state after:
case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
m n : ℕ
hm : m ≠ 0
hmn : m ≤ n
hs : s.Nonempty
⊢ #(s ^ m) ≤ #(s ^ n)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
by
  rcases p with ⟨⟩
  simp only [erase_def, coeff]
  exact ite_congr rfl (fun _ ↦ rfl) (fun _ ↦ rfl)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Disjoint p f.ker

pp: case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Codisjoint p f.ker

Tactic:
· rw [disjoint_iff_inf_le]
    rintro x ⟨hpx, hfx⟩
    rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
    simp only [hfx, zero_mem]

Goal state after:
case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Codisjoint p f.ker
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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
u : ↥p
⊢ (ofIsCompl h φ ψ) ↑u = φ u

Tactic:
by simp [ofIsCompl]

Goal state after:
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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
v : ↥q
⊢ (ofIsCompl h φ ψ) ↑v = ψ v

Tactic:
by simp [ofIsCompl]

Goal state after:
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
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
⊢ ofIsCompl h φ ψ = χ

Tactic:
ext x
  obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
  simp [ofIsCompl, hφ, hψ]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : g.range = ⊤
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG

Tactic:
rw [Submodule.map_top, h_surj]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : g.range = ⊤
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ ⊤.FG
Module: Mathlib.Data.ENat.Lattice

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

Tactic:
mul_iInf

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

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
mul_iInf

Goal state after:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ ⨅ i, a * f i = ⨅ i, a * f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Goal state after:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ 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), ⋯⟩
⊢ ↑i < p.length + (q.length + 1)

Tactic:
by exact i.2

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

Goal state before:
pp: case refine_1.left
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
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
⊢ x = y

Tactic:
obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)

Goal state after:
case refine_1.left
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
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ x = y
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
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 : Submodule R M
t : ι → Submodule R N
⊢ map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)

Tactic:
by
  suffices map₂ f (span R s) (⨆ i, span R (t i : Set N)) = ⨆ i, map₂ f (span R s) (span R (t i)) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
x✝ : { f // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
f : ℕ → α
hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv
s : RelSeries r := { length := (RelSeries.longestOf r).length + 1, toFun := fun x ↦ f ↑x, step := ⋯ }
⊢ False

Tactic:
exact (RelSeries.longestOf r).length.lt_succ_self.not_ge s.length_le_length_longestOf

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
⊢ ∃ x, f x = ↑n

Tactic:
obtain ⟨x, hx⟩ := ENat.sSup_mem_of_nonempty_of_lt_top (h ▸ ENat.natCast_lt_top _)
  use x
  simpa [hx] using! h

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊥ ↔ IsEmpty α

Tactic:
by
  rw [eq_bot_iff, krullDim, iSup_le_iff]
  simp only [le_bot_iff, WithBot.natCast_ne_bot, isEmpty_iff]
  exact ⟨fun H x ↦ H ⟨0, fun _ ↦ x, by simp⟩, (· <| · 1)⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ t₂ : M ⊗[R] N
⊢ t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
    t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → t₁ + t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
ht₁

Goal state after:
case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ t₂ : M ⊗[R] N
ht₁ : t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
⊢ t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → t₁ + t₂ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
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
⊢ Submodule.map₂ (mk R P Q) p.subtype.range q.subtype.range = Submodule.map₂ (mk R P Q) p q

Tactic:
Submodule.range_subtype

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ t • 0 ∈ ⨆ i, T • S i

Tactic:
by simp_rw [smul_zero]; apply zero_mem

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T = closure (S * T)

Tactic:
by
  apply le_antisymm
  · refine mul_le.2 fun a ha b hb => ?_
    rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
    refine (closure_le.2 fun a' ha' => ?_) ha
    change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
    refine (closure_le.2 fun b' hb' => ?_) hb
    change a' * b' ∈ closure (S * T)
    exact subset_closure (Set.mul_mem_mul ha' hb')
  · rw [closure_le]
    rintro _ ⟨a, ha, b, hb, rfl⟩
    exact mul_mem_mul (subset_closure ha) (subset_closure hb)

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

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

Tactic:
rw [add_comm] at h
  exact h.of_add_mul_left_right

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

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

Tactic:
inv_mul_cancel,

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ 1 • (a * y) + b * z = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
h : ∀ i ∈ Finset.cons b t hbt, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ Finset.cons b t hbt, s i) x

Tactic:
Finset.prod_cons

Goal state after:
case cons
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
h : ∀ i ∈ Finset.cons b t hbt, IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x
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
| ⊤

Tactic:
← Submodule.one_mul ⊤,

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
| 1 * ⊤
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:
obtain rfl | hn := Decidable.eq_or_ne n 0

Goal state after:
case inl
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
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid

case inr
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 : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ∈ nonZeroDivisors S
⊢ x * y ∈ x • p ↔ y ∈ p

Tactic:
by
  simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]

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

Goal state before:
pp: case cons.mpr
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)) →
    ∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1

Tactic:
· rintro ⟨hs, Hb⟩
      obtain ⟨μ, hμ⟩ := ih.mpr hs
      obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
      use fun i ↦ if i = a then u else v * μ i
      have hμ' : (∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)) = v * s a := by
        rw [← mul_sum, ← sum_mul, hμ, one_mul]
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]
      simp only [↓reduceIte, ite_mul]
      rw [← huv, ← hμ', sum_congr rfl]
      intro x hx
      rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
      rw [mul_assoc]
      congr
      rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
      congr 2
      rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

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
ji : ¬j = i
⊢ IsRelPrime (s i) (s j)

Tactic:
exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm

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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∏ i ∈ s, span R (M i) = span R (∏ i ∈ s, M i) → ∏ i ∈ insert a s, span R (M i) = span R (∏ i ∈ insert a s, M i)

Tactic:
intro _ _ H ih
    rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 ≤ 1 / I ↔ I ≤ 1

Tactic:
le_div_iff_mul_le,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 * I ≤ 1 ↔ I ≤ 1
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.snd R S) '' s ×ˢ t ⊆ t

Tactic:
exact Set.snd_image_prod_subset _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I J : Submodule R A
⊢ 1 ≤ I / J ↔ J ≤ I

Tactic:
le_div_iff_mul_le,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I J : Submodule R A
⊢ 1 * J ≤ I ↔ J ≤ I
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)
⊢ x ∈ s • restrictScalars S N

Tactic:
restrictScalars_mem

Goal state after:
case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ x ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
M₁ M₂ : Submodule R N
inst✝¹ : IsNoetherian R ↥M₁
inst✝ : IsNoetherian R ↥M₂
this : IsNoetherian R ↥(M₁ ⊔ M₂.subtype.range)
⊢ IsNoetherian R ↥(M₁ ⊔ M₂)

Tactic:
Submodule.range_subtype

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
M₁ M₂ : Submodule R N
inst✝¹ : IsNoetherian R ↥M₁
inst✝ : IsNoetherian R ↥M₂
this : IsNoetherian R ↥(M₁ ⊔ M₂)
⊢ IsNoetherian R ↥(M₁ ⊔ M₂)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
intro _ _ e h _ _; rw [← e.iSup_comp]; apply h

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

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (N ⧸ S)
⊢ S.subtype.range = S

Tactic:
Submodule.range_subtype

Goal state after:
R : Type u_1
N : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
S : Submodule R N
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (N ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (N ⧸ S)
⊢ S = S
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
N : Submodule R M
x : ↥N
⊢ I • N.subtype.range = I • N

Tactic:
Submodule.range_subtype

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ I • N = I • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (f.symm.toRingHom.comp f.toRingHom) I = I

Tactic:
RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map ((↑f.symm).comp f.toRingHom) I = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map ((↑f.symm).comp f.toRingHom) I = I

Tactic:
RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map ((↑f.symm).comp ↑f) I = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (f.symm.toRingHom.comp f.toRingHom) I = I

Tactic:
RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap ((↑f.symm).comp f.toRingHom) I = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap ((↑f.symm).comp f.toRingHom) I = I

Tactic:
RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap ((↑f.symm).comp ↑f) I = I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ Ideal.comap f (ker e.toRingHom) = ker f

Tactic:
RingEquiv.toRingHom_eq_coe,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ Ideal.comap f (ker ↑e) = ker f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ker f = ⊥

Tactic:
rw [SetLike.ext'_iff, ker_eq, Set.ext_iff]

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ∀ (x : R), x ∈ ⇑f ⁻¹' {0} ↔ x ∈ ↑⊥