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

Goal state before:
pp: α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))

Tactic:
← List.append_assoc,

Goal state after:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ (L₁✝ ++ L₂✝))
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
L₅ : List (α × Bool)
H3 : Step (tl ++ x✝⁵) L₅
H4 : Step (tl2 ++ x✝⁴) L₅
⊢ Step ((x4, b4) :: tl2 ++ x✝⁴) ((x3, b3) :: L₅)

Tactic:
by simpa [H1] using Step.cons H4

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ s ∪ t, f x = ∏ i, f i

Tactic:
← Finset.sup_eq_union,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ s ⊔ t, f x = ∏ i, f i
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
simp [nil_iff] at h₁

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case cons
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
· cases eq
    change Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
    apply append_append _ h₂
    have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
    have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
    rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
    rw [red_iff_irreducible H1] at h₁
    rwa [h₁] at h₂

Goal state after:
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ b⁻¹ ∈ s

Tactic:
s.inv_mem_iff

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ b ∈ s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
⊢ f = g

Tactic:
by
  ext x
  have this (x) : f (of x)⁻¹ = g (of x)⁻¹ := by
    trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
    · simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
    · simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
  induction x <;> simp [*]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
⊢ x✝¹ = x✝

Tactic:
let ⟨L₁, hx, hy⟩ := Red.exact.1 H

Goal state after:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝

Tactic:
simp [Red.singleton_iff] at hx hy

Goal state after:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
· rw [hb h₂, mul_one]
    apply prod_eq_single_of_mem a h₁
    exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ ↑x = 1 ↔ x ∈ N

Tactic:
refine QuotientGroup.eq.trans ?_
  rw [mul_one, Subgroup.inv_mem_iff]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ S_1.Finite

Tactic:
refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩

Goal state after:
case mp
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid
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
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ r₂ s₂

Tactic:
hP r₁ t₁ s₁ ht₁ r₂ 1 s₂ (by simp)

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
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (1 • r₂) ⟨1 * ↑s₂, ⋯⟩ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ r₂ s₂
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

Tactic:
by
  rw [mul_comm]
  exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.domRestrict S) h y)

Goal state after:
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_2
inst✝ : MulAction R X
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
by
  cases x with | _ r s
  simp [OreLocalization.one_def, oreDiv_smul_char 1 r 1 s 1 s (by simp)]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.mk' (x * ↑y) y = f x

Tactic:
by
  rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ↑a * ⊤ = Option.bind ⊤ fun b ↦ Option.some (a * b)

Tactic:
by simp [ha]; rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case h
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ f x.1 * f (↑x.2)⁻¹ = m

Tactic:
← eq,

Goal state after:
case h
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ m * f ↑x.2 * f (↑x.2)⁻¹ = m
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
convert! exists_pred_iterate_of_le h.ofDual

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : IsMax a
⊢ succ a ≤ b ↔ a < b

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b

Tactic:
· grind [le_succ, IsMax.mono]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ a < succ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b

Tactic:
exact hd'.trans_le (hb hd)

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a

Tactic:
rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + 1 < x

Tactic:
rw [← succ_eq_add_one]
  exact hx.succ_lt hy

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + (↑n + 1) < x

Tactic:
← add_assoc

Goal state after:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑n + 1 < x
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ (m - ↑n).toNat = m.toNat - (↑n).toNat

Tactic:
induction m

Goal state after:
case top
n : ℕ
⊢ (⊤ - ↑n).toNat = ⊤.toNat - (↑n).toNat

case coe
n a✝ : ℕ
⊢ (↑a✝ - ↑n).toNat = (↑a✝).toNat - (↑n).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ m.toNat = n ↔ m = ↑n

Tactic:
induction m

Goal state after:
case top
n : ℕ
hn : n ≠ 0
⊢ ⊤.toNat = n ↔ ⊤ = ↑n

case coe
n : ℕ
hn : n ≠ 0
a✝ : ℕ
⊢ (↑a✝).toNat = n ↔ ↑a✝ = ↑n
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(pred a) = pred ↑a

Tactic:
change Subtype.val (dite ..) = _
  simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable ((a : α) → π a)

Tactic:
have (n : ℕ) : Countable (Fin n → ℕ) := by
    induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)

Goal state after:
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
⊢ Countable ((a : α) → π a)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
apply Vector.eq

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
by
  rcases n with - | n
  · exact i.elim0
  induction n generalizing b with
  | zero =>
    have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
  | succ n hn =>
    rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ (if ↑i ≤ (↑v).length then (↑v).length + 1 else (↑v).length) = n + 1

Tactic:
v.2

Goal state after:
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ (if ↑i ≤ n then n + 1 else n) = n + 1
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ c✝ : α
hab : a✝ ≤ c✝
hba : ¬inl c✝ ≤ inl a✝
⊢ inl a✝ < inl c✝

case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : IsMin (sSup s) ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
rcases hlim with (hmin | hlim)

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
⊢ sSup s ∈ s

case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a → ∃ c ≤ a, f c = b

Tactic:
intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ IsLUB (Function.const α x '' s) (Function.const α x a✝¹)

Tactic:
simp [IsLUB, IsLeast, upperBounds, lowerBounds]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ ∀ ⦃a : β⦄, (∀ a_1 ∈ s, x ≤ a) → x ≤ a
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o

Tactic:
by
  simp [map, Function.comp_assoc]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : Part α
⊢ x.bind some = x

Tactic:
rw [bind_some_eq_map]

Goal state after:
α : Type u_1
x : Part α
⊢ map (fun y ↦ y) x = x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

Tactic:
dif_pos h'

Goal state after:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h')
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ i ≤ max i j

Tactic:
apply le_max_left

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ sum (f + g) = sum f + sum g

Tactic:
by
  have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
  simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
  exact this

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

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ (y * x).toENatAux = x.toENatAux * y.toENatAux

Tactic:
this y x (le_of_not_ge hle),

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ y.toENatAux * x.toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ (y + x).toENatAux = x.toENatAux + y.toENatAux

Tactic:
this y x (le_of_not_ge hle),

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ y.toENatAux + x.toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c

Tactic:
intro c hc
    by_contra h
    obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le
    simp_rw [lift_le] at h hc
    rw [csSup_le_iff' hs] at h
    exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 2 ≤ c ↔ 1 < c

Tactic:
by
  convert! natCast_add_one_le_iff
  norm_cast

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Finite α
⊢ ∃ s, n = s.card

pp: case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card

Tactic:
· let hα := Fintype.ofFinite α
    obtain ⟨t, -, rfl⟩ := @Finset.exists_subset_card_eq α .univ n <| by simpa using h
    exact ⟨t, rfl⟩

Goal state after:
case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a
  simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]
  simp only [and_comm, or_comm]

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:
rw [lift_mk_le.{0}]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).1 = x✝.1

Tactic:
exact one_smul ..

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).2 = x✝.2

Tactic:
exact one_smul ..

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
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a

Tactic:
rcases dvd_or_dvd hp h with dvd_a | dvd_pow

Goal state after:
case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Tactic:
rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)

Goal state after:
case refine_2.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

case refine_2.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Quot.out (Associates.mk a) ~ᵤ a

Tactic:
← Associates.mk_eq_mk_iff_associated,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk (Quot.out (Associates.mk a)) = Associates.mk a
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✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
x : M
hx : f x = y
hx' : x ∈ p
hxz : z + x ∈ p
this : z + x - x ∈ p
⊢ z ∈ p

Tactic:
simpa only [this, add_sub_cancel_right]

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₂
⊢ f.rangeRestrict.range = ⊤

Tactic:
range_rangeRestrict

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₂
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case closed_under_smul
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ ∀ ⦃r_1 : S⦄ ⦃n : M⦄, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ r • N

Tactic:
rintro _ m rfl hm; exact ⟨m, hm, rfl⟩

Goal state after: