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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : 1 < #A * #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
by
    simp_rw [Nat.one_lt_mul_iff, card_pos] at hc
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty hc.1 hc.2.1
    let C := A.map ⟨_, mul_right_injective a⁻¹⟩ -- C = a⁻¹A
    let D := B.map ⟨_, mul_left_injective b⁻¹⟩  -- D = Bb⁻¹
    have hcard : 1 < #C ∨ 1 < #D := by simp_rw [C, D, card_map]; exact hc.2.2
    have hC : 1 ∈ C := mem_map.mpr ⟨a, ha, inv_mul_cancel a⟩
    have hD : 1 ∈ D := mem_map.mpr ⟨b, hb, mul_inv_cancel b⟩
    suffices ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d by
      simp_rw [mem_product]
      obtain ⟨c, hc, d, hd, hne, hu'⟩ := this
      obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
      obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
      refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
      · simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
        rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
      specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
      simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
      rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
      exact hu' rfl
    classical
    let _ := Finset.mul (α := G)              -- E = D⁻¹C, F = DC⁻¹
    have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
    · obtain ⟨e, he, f, hf, hu⟩ := this
      clear_value C D
      simp only [UniqueMul, mem_mul, mem_image] at he hf hu
      obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he
      obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
      by_cases! h12 : c1 ≠ 1 ∨ d2 ≠ 1
      · refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
        rw [mul_left_cancel_iff, mul_right_cancel_iff,
            mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu; exact hu rfl
      obtain ⟨rfl, rfl⟩ := h12
      by_cases! h21 : c2 ≠ 1 ∨ d1 ≠ 1
      · refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
        simpa only [mul_one, one_mul, ← mul_inv_rev, he, true_imp_iff, inv_inj, and_comm] using hu
      obtain ⟨rfl, rfl⟩ := h21
      rcases hcard with hC | hD
      · obtain ⟨c, hc, hc1⟩ := exists_mem_ne hC 1
        refine (hc1 ?_).elim
        simpa using hu ⟨_, ⟨_, hD, rfl⟩, _, hc, rfl⟩ ⟨_, hD, _, ⟨_, hc, rfl⟩, rfl⟩
      · obtain ⟨d, hd, hd1⟩ := exists_mem_ne hD 1
        refine (hd1 ?_).elim
        simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩
    all_goals apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
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
⊢ ⊤ ≤ p ⊔ f.ker

Tactic:
intro x _

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
x : E
a✝ : x ∈ ⊤
⊢ x ∈ p ⊔ f.ker
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
⊢ x ∈ Set.range f → (g' ∘ g) x = 1

Tactic:
intro H

Goal state after:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
⊢ (g' ∘ g) x = 1
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
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
⊢ (fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ) = φ

Tactic:
by
      ext x
      · exact ofIsCompl_apply_left h x
      · exact ofIsCompl_apply_right h x

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a ≤ c + ⨅ i, f i ↔ ⨆ i, a - f i ≤ c

Tactic:
add_comm,

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a ≤ (⨅ i, f i) + c ↔ ⨆ i, a - f i ≤ c
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
add_comm,

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ iInf f + a = ⨅ b, a + f b
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p2.1} = A
⊢ 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
    ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
        p1 ≠ p2_1 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
            UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2

Tactic:
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

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

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p1.1} = A
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2

Tactic:
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ i.succ.castSucc.insertNth a p.toFun m.succ = p.toFun ⟨↑m - 1, ⋯⟩.succ

Tactic:
Fin.insertNth_apply_above

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun ⟨↑m - 1, ⋯⟩.succ

case e'_4.h
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ i.succ.castSucc < m.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ i.succ.castSucc.insertNth a p.toFun m.succ = p.toFun i.succ

Tactic:
Fin.insertNth_apply_above

Goal state after:
case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ ⋯ ▸ p.toFun (m.succ.pred ⋯) = p.toFun i.succ

case e'_4.h
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ i.succ.castSucc < m.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
intro H

Goal state after:
case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∀ (n : ℕ), ∃ x, x.length = n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
intro H

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
⊢ ∀ (x : RelSeries r), ∃ y, x.length < y.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ ⟨⟨lf, f⟩, mf⟩ = ⟨⟨lf, g⟩, mg⟩

Tactic:
simp_rw [Subtype.mk_eq_mk, Sigma.mk.inj_iff, heq_eq_eq, true_and]

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ f = g
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ ↑(p.cons x hx).length ≤ coheight a

Tactic:
RelSeries.cons_length,

Goal state after:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
p : RelSeries {(a, b) | a < b}
x : β
hx : (x, p.head) ∈ {(a, b) | a < b}
ih : ∀ (a : α), p.head = f a → ↑p.length ≤ coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' : f a' = p.head
⊢ ↑(p.length + 1) ≤ coheight a
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_1.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length)
⊢ j.castSucc = Fin.last { length := n + 1, toFun := s, step := h }.length

Tactic:
eq_comm

Goal state after:
case succ.refine_1.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length) j.castSucc
⊢ j.castSucc = Fin.last { length := n + 1, toFun := s, step := h }.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) → ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
rintro ⟨⟨_ | _ | n, l, hl⟩, hl'⟩
    iterate 2 · cases hl'.not_ge (by simp)
    exact ⟨l 1, ⟨l 0, hl 0⟩, l 2, hl 1⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
⊢ InfiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

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

Tactic:
simpa [krullDim_eq_top] using SetRel.InfiniteDimensional.exists_relSeries_with_length n

Goal state after:
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
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ n * r ^ l = r ^ n
⊢ n = n + l

Tactic:
IsLeftRegular.mul_left_eq_self_iff (hx.pow n),

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : r ^ l = 1
⊢ n = n + l
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ b + (a + b) = a + b

Tactic:
add_comm,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ a + b + b = a + b
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
H✝ : IsCoprime x y
a b : R
H : a * x + b * y = 1
⊢ b * y + a * x = 1

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : R
H✝ : IsCoprime x y
a b : R
H : a * x + b * y = 1
⊢ a * x + b * y = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y

Tactic:
by
  rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y

Tactic:
by
  rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]

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

Goal state before:
pp: case mp
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = a * m + b * n

Tactic:
eq_comm

Goal state after:
case mp
m n a b : ℤ
h : a * m + b * n = 1
⊢ a * m + b * n = ↑1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
x y : ℤ
h : IsCoprime x y
⊢ y * x.gcdB y + x.gcdA y * x = 1

Tactic:
add_comm,

Goal state after:
case h
x y : ℤ
h : IsCoprime x y
⊢ x.gcdA y * x + y * x.gcdB y = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x

Tactic:
classical
  refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]

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
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ M ^ (n + 1) = M * M ^ n

Tactic:
add_comm,

Goal state after:
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 : ℕ
h : n ≠ 0
⊢ M ^ (1 + n) = M * M ^ n
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) ⋯
r : R
hx✝ : (Algebra.algebraMap R A) r ∈ M ^ 0
hx : (Algebra.algebraMap R A) r ∈ 1
⊢ C 0 ((Algebra.algebraMap R A) r) hx✝

Tactic:
exact algebraMap r

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) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
r : R
hx✝ : (Algebra.algebraMap R A) r ∈ M ^ 0
hx : (Algebra.algebraMap R A) r ∈ 1
⊢ C 0 ((Algebra.algebraMap R A) r) hx✝

Tactic:
exact algebraMap r

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
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ u, (algebraMap R A) ↑u = x✝

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : A
⊢ x✝ ∈ MonoidHom.mker (spanSingleton R) ↔ ∃ u, x✝ = (algebraMap R A) ↑u
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx : x ∈ {x | ∀ y ∈ J, x * y ∈ I}
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I

Tactic:
exact Submodule.smul_mem _ _ (hx _ hy)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥

Tactic:
by
  rw [← prod_inj, prod_bot_bot]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.IsPrime
x y : R × S
⊢ x * y ∈ I.prod ⊤ → x ∈ I.prod ⊤ ∨ y ∈ I.prod ⊤

Tactic:
simpa using h.mem_or_mem

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal (Ideal.prod (R ∙ generator (Ideal.map (RingHom.fst R S) I)) (Ideal.map (RingHom.snd R S) I))

Tactic:
← span_singleton_generator (I.map (RingHom.snd R S)),

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    (Ideal.prod (R ∙ generator (Ideal.map (RingHom.fst R S) I)) (S ∙ generator (Ideal.map (RingHom.snd R S) I)))
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
mul_comm (_ / _),

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬a * b - b * (a * b / b) ≺ b
⊢ False
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
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝³ x✝² : R
x✝¹ : x✝³ ∈ span R S
x✝ : x✝² ∈ span R S
h₁ : x✝³ • m ∈ span R (S • T)
h₂ : x✝² • m ∈ span R (S • T)
⊢ (x✝³ + x✝²) • m ∈ span R (S • T)

Tactic:
by rw [add_smul]; exact add_mem h₁ h₂

Goal state after: