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

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
by simpa only [comm₁₂] using hy₁

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

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
hx₂ : g x₂ = 1
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
by simpa only [comm₁₂] using hy₁

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
by
  simp_rw [iInf_add, add_iInf]; exact le_iInf₂ h

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 ∘ₗ T) ∘ₗ f = f ∘ₗ T

Tactic:
hf.comp_eq_left_iff,

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 ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
hc : 1 < #A✝ * #B✝
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
⊢ ∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2

Tactic:
rw [← card_map f, ← card_map f, mul_comm] at hc

Goal state after:
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 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2
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✝
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 : M
y : P
⊢ ∃ a, ((↑l).prod g) a = (x, y)

Tactic:
obtain ⟨y, rfl⟩ := hg y

Goal state after:
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✝
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 : M
y : N
⊢ ∃ a, ((↑l).prod g) a = (x, g y)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ fromListIsChain (x :: l) ⋯ ⋯ = (fromListIsChain l l_ne_nil hl).cons x ⋯

Tactic:
apply toList_injective

Goal state after:
α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
x : α
hx : (x, l.head l_ne_nil) ∈ r
⊢ (fromListIsChain (x :: l) ⋯ ⋯).toList = ((fromListIsChain l l_ne_nil hl).cons x ⋯).toList
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

Tactic:
by
  simp only [snoc, append, mem_def, Set.mem_range]
  constructor
  · rintro ⟨i, rfl⟩
    exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i
  · intro h
    rcases h with (⟨i, rfl⟩ | rfl)
    · exact ⟨i.castSucc, Fin.append_left _ _ _⟩
    · exact ⟨Fin.last _, Fin.append_right _ _ 0⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ (p.cons x hx).tail ⋯ = p

Tactic:
apply toList_injective

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ ((p.cons x hx).tail ⋯).toList = p.toList
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ (p.tail hp).cons p.head ⋯ = p

Tactic:
apply toList_injective

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ ((p.tail hp).cons p.head ⋯).toList = p.toList
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.eraseLast.snoc p.last ⋯ = p

Tactic:
apply toList_injective

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ (p.eraseLast.snoc p.last ⋯).toList = p.toList
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ + 1 ≤ height b

Tactic:
have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
    simp [this]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length ≤ ⊥ ↔ IsEmpty α

Tactic:
iSup_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ ⊥) ↔ IsEmpty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length ≤ 1 ↔ ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b

Tactic:
iSup_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ 1) ↔ ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b
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✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ (r • 1 • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • 1 • n)

Tactic:
← smul_assoc,

Goal state after:
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✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ ((r • 1) • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • 1 • n)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
by
  cases isEmpty_or_nonempty α
  · simp [krullDim_eq_bot]
  cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
  · rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]
    constructor
    · exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩
    · exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest
  · simpa [krullDim_eq_top] using SetRel.InfiniteDimensional.exists_relSeries_with_length n

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : LTSeries α), ↑i.length ≤ ↑(⨆ a, height a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ i, ↑(height i) ≤ krullDim α

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : α), ↑(height i) ≤ krullDim α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ⨆ a, height a + coheight a ≤ ⨆ p, ↑p.length

Tactic:
apply iSup_le

Goal state after:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ∀ (i : α), height i + coheight i ≤ ⨆ p, ↑p.length
Module: Mathlib.Order.KrullDimension

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

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), ⨆ (_ : RelSeries.last i ≤ x), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ RelSeries.last p ≤ x → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length
Module: Mathlib.Order.KrullDimension

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

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries ↑(Set.Iic x)), ⨆ (_ : RelSeries.last i ≤ ⊤), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
apply iSup_le

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ RelSeries.last p ≤ ⊤ → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
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
⊢ ⨆ a, ↑(height a) ≤ ((↑m + 1) * ⨆ a, ↑(height a)) + ↑m

Tactic:
iSup_le_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
⊢ ∀ (i : α), ↑(height i) ≤ ((↑m + 1) * ⨆ a, ↑(height a)) + ↑m
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: 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 : α
⊢ (∃ x ∈ f i, ∃ y ∈ ∏ x ∈ is, f x, x * y = a) ↔
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a

Tactic:
ih

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 : α
⊢ (∃ x ∈ f i, ∃ y, (∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = y) ∧ x * y = a) ↔
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), g i * ∏ i ∈ is, g i = a
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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

Tactic:
by
  simp_rw [mapIncl, range_map, Submodule.range_subtype]

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

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a

Tactic:
succ_nsmul,

Goal state after:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 1) • a + a = a
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:
nth_rw 1 [← 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.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: 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
f : M →ₗ[R] M
n : ℕ
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
by
  have h := TensorProduct.map_pow f (id : N →ₗ[R] N) n
  rwa [Module.End.id_pow] at h

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ 1 = closure 1

Tactic:
one_eq_closure_one_set

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : Set R
⊢ closure 1 = closure 1
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : b * a ≤ b
⊢ b * a∗ ≤ b

Tactic:
rw [← le, mul, kstar]
    rw [← le, mul] at h
    exact mul_kstar_le_self h

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
⊢ comap (↑(opLinearEquiv R).symm) 1 = 1

Tactic:
← map_equiv_eq_comap_symm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ map (↑(opLinearEquiv R)) 1 = 1
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
M N : Submodule R A
⊢ comap (↑(opLinearEquiv R).symm) (M * N) = comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M

Tactic:
← map_equiv_eq_comap_symm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
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
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑((opLinearEquiv R).symm ≪≫ₗ opLinearEquiv R)) (M * N) =
    map (↑((opLinearEquiv R).symm ≪≫ₗ opLinearEquiv R)) M * map (↑((opLinearEquiv R).symm ≪≫ₗ opLinearEquiv R)) N

Tactic:
LinearEquiv.symm_trans_self,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) (M * N) = map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ)) N
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
⊢ ((↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z) →
    (↑(insert a r)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a r, s i ∣ z) → ∏ x ∈ insert a r, s x ∣ z

Tactic:
ih

Goal state after:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
⊢ (↑(insert a r)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a r, s i ∣ z) → ∏ x ∈ insert a r, s x ∣ z
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 ι
H : 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:
ih

Goal state after:
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 ι
H : a✝ ∉ s✝
ih : ∏ 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)
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
inst✝ : Fintype α✝
⊢ (∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)) →
    ∀ {M : Option α✝ → Submodule R N} [∀ (i : Option α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
ih

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
ι : Type u_6
inst✝¹ : Finite ι
α✝ : Type u_6
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R N} [∀ (i : α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
⊢ ∀ {M : Option α✝ → Submodule R N} [∀ (i : Option α✝), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (a, 1, 0)

Tactic:
dsimp [P]; rw [mul_one, mul_zero, add_zero]

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

Goal state before:
pp: case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

Tactic:
rw [← sub_eq_zero]
    exact H (Module.mem_annihilator (r := r - s).mpr
      (by simp only [sub_smul, H', sub_self, implies_true]))

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (map (fun x ↦ a * x) s).gcd = GCDMonoid.gcd (a * b) (a * s.gcd)

Tactic:
ih

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (normalize a * s.gcd) = GCDMonoid.gcd (a * b) (a * s.gcd)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J * J ^ n = ⊤

Tactic:
sup_mul_eq_of_coprime_right ih

Goal state after:
case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J = ⊤
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.lcm f = s₂.lcm g

Tactic:
subst hs
  exact Finset.fold_congr hfg

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.gcd f = s₂.gcd g

Tactic:
subst hs
  exact Finset.fold_congr hfg

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
⊢ s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
ih

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ (a ::ₘ s).prod ≤ (a ::ₘ s).inf
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
u : αˣ
a✝ : Nontrivial α
⊢ a = 0 → normalize a = normalize (a * ↑u)

Tactic:
rintro rfl; simp only [zero_mul]

Goal state after: