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

Goal state before:
pp: case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih : motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (Polynomial.C (p.coeff n) * X ^ n + ∑ x ∈ s, Polynomial.C (p.coeff x) * X ^ x)

Tactic:
exact add _ _ A ih

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff n = a

Tactic:
rw [p.coeff_update_apply, if_pos rfl]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : IsDomain R
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R fun i ↦ single i (v i)

Tactic:
by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact linearIndependent_single (f := fun i (_ : Unit) ↦ v i) <| by simp +contextual [hv]

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

Goal state before:
pp: case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.1 = y.1

Tactic:
apply up_injective

Goal state after:
case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.1 } = { down := y.1 }
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.2 = y.2

Tactic:
apply up_injective

Goal state after:
case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : UniqueProds G
inst✝ : UniqueProds H
this : ∀ (b : Bool), UniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.2 } = { down := y.2 }
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: 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
⊢ f x ∈ map f s

Tactic:
mem_map

Goal state after:
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
⊢ ∃ y ∈ s, f y = f x
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
this : Inhabited P
⊢ (lmapDomain R R g) l ∈ map (lmapDomain R R g) (supported R R ↑t1)

Tactic:
mem_map

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
this : Inhabited P
⊢ ∃ y ∈ supported R R ↑t1, (lmapDomain R R g) y = (lmapDomain R R g) l
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
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
x : F
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Tactic:
by
  obtain ⟨ix, rfl⟩ := (LinearEquiv.ofInjective i hi).symm.surjective x
  simp [linearProjOfIsCompl]

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

Goal state before:
pp: case refine_1.right
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
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
intro x
      obtain ⟨y, hy⟩ := (h (x - l.1 (g x))).mp (by simp [h₁, g.map_sub])
      exact ⟨⟨y, g x⟩, by simp [hy]⟩

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

Goal state before:
pp: case refine_1.right
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
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
· intro x
      obtain ⟨y, hy⟩ := (h (x - l.1 (g x))).mp (by simp [h₁, g.map_sub])
      exact ⟨⟨y, g x⟩, by simp [hy]⟩

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

Goal state before:
pp: case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.1 = y.1

Tactic:
apply up_injective

Goal state after:
case refine_1.refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.1 } = { down := y.1 }
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ x.2 = y.2

Tactic:
apply up_injective

Goal state after:
case refine_1.refine_2
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he : (Prod.upMulHom G H) x = (Prod.upMulHom G H) y
⊢ { down := x.2 } = { down := y.2 }
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_5
G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝
h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝
hne : (p1.2.1, p1.1.1).1 = (p2.2.1, p2.1.1).1 ∧ (p1.2.1, p1.1.1).2 = (p2.2.1, p2.1.1).2
⊢ p1.1 = p2.1 ∧ p1.2 = p2.2

Tactic:
exact ⟨unop_injective hne.2, unop_injective hne.1⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inl
α : 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
⊢ (x, y) ∈ r

pp: case inr.inl
α : 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
⊢ (x, y) ∈ r

pp: case inr.inr
α : 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 < ↑m
⊢ (x, y) ∈ r

Tactic:
· convert! p.step ⟨m, hm.trans i.2⟩
      · change Fin.insertNth _ _ _ _ = _
        rw [Fin.insertNth_apply_below]
        pick_goal 2
        · exact hm.trans (lt_add_one _)
        simp
      · change Fin.insertNth _ _ _ _ = _
        rw [Fin.insertNth_apply_below]
        pick_goal 2
        · change m.1 + 1 < i.1 + 1; rwa [add_lt_add_iff_right]
        simp; rfl

Goal state after:
case inr.inl
α : 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
⊢ (x, y) ∈ r

case inr.inr
α : 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 < ↑m
⊢ (x, y) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inl
α : 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
⊢ (p.toFun m, y) ∈ r

Tactic:
convert! prev_connect

Goal state after:
case e'_3
α : 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 = i.castSucc

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 : ↑m = ↑i
⊢ y = a
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.eraseLast.toList ++ [p.last] = p.toList

Tactic:
← getLast_toList,

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.eraseLast.toList ++ [p.toList.getLast ⋯] = p.toList
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length

Tactic:
apply eq_of_forall_ge_iff
  intro n
  rw [height_le_iff', iSup₂_le_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ f.range = ⊤

Tactic:
LinearMap.range_eq_top

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ Function.Surjective ⇑f
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Tactic:
simp [ENat.WithBot.lt_add_one_iff, WithBot.coe_natCast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
· rw [height_add_const]
    apply iSup₂_le
    intro p hlast
    let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)
    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMulCommClass R R' M
inst✝² : SMulCommClass R R'' M
inst✝¹ : Module R''ᵐᵒᵖ M
inst✝ : IsCentralScalar R'' M
r : R''
x✝ x y : M ⊗[R] N
hx : MulOpposite.op r • x = r • x
hy : MulOpposite.op r • y = r • y
⊢ MulOpposite.op r • (x + y) = r • (x + y)

Tactic:
rw [smul_add, smul_add, hx, hy]

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

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

Tactic:
induction t using Finset.induction_on generalizing a with

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ a ∈ ∏ i ∈ insert i is, f i ↔ ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
⊢ Function.Injective fun n ↦ r ^ n

Tactic:
by
  intro n m hnm
  have main {n m} (h₁ : n ≤ m) (h₂ : r ^ n = r ^ m) : n = m := by
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le h₁
    rw [pow_add, eq_comm, IsLeftRegular.mul_left_eq_self_iff (hx.pow n), pow_eq_one_iff_right hx']
      at h₂
    rw [h₂, Nat.add_zero]
  obtain h | h := Nat.le_or_le n m
  · exact main h hnm
  · exact (main h hnm.symm).symm

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (map f g).range = Submodule.map₂ (mk R P Q) f.range g.range

Tactic:
← Submodule.map_top,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map (map f g) ⊤ = Submodule.map₂ (mk R P Q) (Submodule.map f ⊤) (Submodule.map g ⊤)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y ∈ a, ∃ a, a • y = x) → x ∈ a

Tactic:
rintro ⟨y, hy, r, rfl⟩
      exact smul_mem _ _ hy

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

Goal state before:
pp: case cons
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)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
pairwise_cons'

Goal state after:
case cons
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)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
i j k : Fin n
⊢ min (toInt val i) (toInt val j) = toInt val k ↔ min (val i) (val j) = val k

Tactic:
by
  simp [le_antisymm_iff, inf_le_iff, le_inf_iff, toInt_le_toInt]

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
⊢ map₂ (LinearMap.mul R A) s t = span R (↑s * ↑t)

Tactic:
exact map₂_eq_span_image2 _ s t

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
P : Type u_7
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N), Submodule.comap g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ f.range

Tactic:
simp [Submodule.comap_map_eq, h]

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

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

Tactic:
by_contra h

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').1 = gcd x y

Tactic:
simp only [xgcdAux_rec h, IH]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
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
y : S
⊢ f.symm y ∈ I ↔ y ∈ map f I

Tactic:
rw [← comap_symm, mem_comap]

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal S
φ : Ideal S ↪o Ideal R := orderEmbeddingOfSurjective f hf
J : Ideal S
K : Ideal R
h : φ J < K
⊢ J < map f K

Tactic:
rw [← J.map_comap_of_surjective f hf]
    apply lt_of_le_not_ge (map_mono h.le)
    simpa [map_le_iff_le_comap, φ] using h.not_ge

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

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

Tactic:
rintro x ⟨y, hy, x, ⟨i, rfl⟩, rfl⟩

Goal state after:
case mp.refine_1
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
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = (fun x1 x2 ↦ x1 • x2) y (f i)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y / gcd x y ∣ z

Tactic:
suffices x * y ∣ z * gcd x y by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * gcd x y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ Ideal.span {r} • N = r • N

Tactic:
conv_lhs => rw [← span_eq N, span_smul_span]
  simpa using span_eq (r • N)

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} = J * span {x} ↔ I = J

Tactic:
by
  simp only [le_antisymm_iff, span_singleton_mul_left_mono hx]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
exact (Ideal.mul_le_left.trans (Ideal.mul_le_left.trans
      ((Ideal.pow_le_pow_right hn).trans le_sup_left)))

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
refine (Ideal.mul_le_left.trans (Ideal.mul_le_right.trans
      ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ m ≤ n + m - i