mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)) = (↑s₄' * r₃') • r₂' • r₂ • r₁ /ₒ ⟨↑s₄' * r₃' * ↑(s₂' * s), this⟩

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (↑s₄' * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))) =
    (↑s₄' * (r₃' * (r₂' * r₂))) • r₁ /ₒ ⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i (f z') = i (f w')

Tactic:
← hxz,

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ i (z * f ↑x) = i (f w')
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ (↑s₄' * r₃') • r₁' • x /ₒ ⟨↑s₄' * r₃' * ↑(s₁' * s), this⟩ =
    (s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩))

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_smul, mul_assoc, h₄]

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ (↑s₄' * (r₃' * r₁')) • x /ₒ ⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ =
    (↑s₄' * (r₃' * r₁')) • x /ₒ (s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩)))
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
rw [hb']

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
hb' : (r₂ /ₒ s₂) • (r₃ /ₒ s₃) = rb • r₃ /ₒ (sb * s₂)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : (if a✝ = 0 ∨ b✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a✝ b✝) = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False

Tactic:
if_neg h₂

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : map₂ (fun x1 x2 ↦ x1 * x2) a✝ b✝ = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ a ^ 0 = 1

Tactic:
HPow.hPow,

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ Pow.pow a 0 = 1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
HPow.hPow,

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ Pow.pow a (n + 1) = Pow.pow a n * a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x

Tactic:
bot_mul x0',

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ ≤ b * ↑x
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[m] a)

Tactic:
exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
Ioi_inter_Iio

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ioo a b = Ioo a b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : α
⊢ Option.some a ≤
    match Option.some a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
change _ ≤ ite _ _ _

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : α
⊢ Option.some a ≤ if succ a = a then ⊤ else ↑(succ a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
ha :
  (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ⊤
⊢ IsMax ⊤

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha :
  (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝
⊢ IsMax ↑a✝

Tactic:
· exact isMax_top

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha :
  (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝
⊢ IsMax ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ ¬n.toNat = 0

Tactic:
ENat.toNat_eq_zero,

Goal state after:
n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ ¬(n = 0 ∨ n = ⊤)
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
x✝ : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)

Tactic:
exact (Equiv.sumCompl (· = a)).bijective

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if i = j then f j else 1) = f i

Tactic:
Finset.prod_ite_eq,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (if i ∈ univ then f i else 1) = f i
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : ∀ (a : α), Uncountable (π a)
⊢ Uncountable (Sigma π)

Tactic:
inhabit α; exact Sigma.uncountable default

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)
⊢ False

Tactic:
rw [mem_filter, Sym.mem_coe, mem_replicate] at hb

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i ⟨l, hl⟩) = insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩)

Tactic:
by
    refine Subtype.ext ?_
    simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.val_castAdd]
    apply List.insertIdx_comm
    · assumption
    · rw [hl]
      exact Nat.le_of_succ_le_succ j.2

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ (v.set i a).get j = v.get j

Tactic:
cases v; cases i; cases j
  simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]
  rw [List.getElem_set_of_ne]
  · simpa using h

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simpa using trans_trichotomous_right ha hb

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a

Tactic:
· exact ⟨b, inr_lt_inr_iff.1 h⟩

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b

Tactic:
· exact ⟨b, inr_lt_inr_iff.1 h⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ici a = Ici (e a)

Tactic:
← e.preimage_Ici,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' ⇑e ⁻¹' Ici (e a) = Ici (e a)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy✝ : z ≤ y
hzy : z < y
⊢ f z ≤ y ∨ f y ≤ f z

pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ z ∨ f z ≤ f z

Tactic:
· left; exact hy.map_le_of_mem_of_lt hz hzy

Goal state after:
case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ z ∨ f z ≤ f z
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
ha : (⇑lfp ∘ ⇑h) a = a
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)

Tactic:
calc
    h a a = h a (h a).lfp := congr_arg (h a) ha.symm
    _ = (h a).lfp := (h a).map_lfp
    _ = a := ha

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯

Tactic:
by
  simp [union_def]; aesop

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
⊢ IsChain r (⋃₀ cs)

Tactic:
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
⊢ r y z ∨ r z y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } = { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a →
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
· refine inductionOn₂ a b fun α β h ↦ ?_
    obtain ⟨e⟩ := h.le
    replace e := e.congr (Equiv.refl β) Equiv.ulift
    refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
    apply (e.codRestrict _ mem_range_self).equivOfSurjective
    rintro ⟨a, ⟨b, rfl⟩⟩
    exact ⟨b, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ (n + 1) = c ^ n * c

Tactic:
HPow.hPow,

Goal state after:
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ Pow.pow c (n + 1) = Pow.pow c n * c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1

Tactic:
exact (power_one a).symm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
⊢ False

Tactic:
obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out

Goal state after:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
⊢ False
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ a

Tactic:
exact le_trans (f.monotone h_ind) h_a

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ (toENat c).toNat = 0 ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
ENat.toNat_eq_zero,

Goal state after:
c : Cardinal.{u}
⊢ toENat c = 0 ∨ toENat c = ⊤ ↔ c = 0 ∨ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c < ⊤ ↔ c < ℵ₀

Tactic:
simp [lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
exact Or.inr ⟨sInf s, csInf_mem hne, h⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift.{v, u} #↑(f ⁻¹' s) ≤ lift.{u, v} #↑s

Tactic:
by
  rw [lift_mk_le.{0}]
  use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
  apply Subtype.coind_injective; exact h.comp Subtype.val_injective

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

Tactic:
by
  let p : Submodule R M :=
    { toAddSubmonoid := sSup (toAddSubmonoid '' s)
      smul_mem' := fun t {m} h ↦ by
        simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
        induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem }
  refine le_antisymm (?_ : sSup s ≤ p) ?_
  · exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq
  · exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: M : Type u_4
R : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N₁ N₂ : Submodule R M
⊢ Disjoint N₁ N₂ ↔ ∀ {x y : M}, x ∈ N₁ → y ∈ N₂ → x + y = 0 → x = 0 ∧ y = 0

Tactic:
simp only [← Submodule.mem_toAddSubgroup, ← AddSubgroup.disjoint_iff_add_eq_zero]

Goal state after:
M : Type u_4
R : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N₁ N₂ : Submodule R M
⊢ Disjoint N₁ N₂ ↔ Disjoint N₁.toAddSubgroup N₂.toAddSubgroup
Module: Mathlib.Algebra.Ring.Centralizer

Goal state before:
pp: M : Type u_1
S : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * (a + b) = (a + b) * c

Tactic:
by rw [add_mul, mul_add, ha c hc, hb c hc]

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

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
| add_right _ _ _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : CharZero R
⊢ FaithfulSMul ℕ R

Tactic:
simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| add_right _ _ _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
⊢ ¬Irreducible (x ^ (n + 2))

Tactic:
intro ⟨h₁, h₂⟩
    have := h₂ (pow_succ _ _)
    rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this
    exact h₁ (this.pow _)

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
obtain ⟨y, hy, hxy⟩ := hx

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : f y = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ s = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rwa [left_eq_sup, closure_le]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm (x • e 1) = x

Tactic:
by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ f.range = ⊤

Tactic:
LinearMap.range_eq_top_of_surjective f hf

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ ⊤ = ⊤