mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : ¬n < g 0
⊢ False

Tactic:
obtain ⟨n', rfl⟩ := Nat.exists_eq_add_of_le (not_lt.1 hn)
    rw [if_neg hn, add_comm (g 0) n', Nat.add_sub_cancel_right] at hmn
    split_ifs at hmn with hm
    · apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
      exact _root_.trans hmn (List.tail_sublistForall₂_self _)
    · rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn
      apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
      rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
      exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}

Tactic:
refine fun hh g ↦ ⟨?_, ?_⟩ <;> rintro rfl

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {g}
⊢ h * g * h⁻¹ ∈ {g}

case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g ∈ {h * g * h⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯
x : G
⊢ ∀ (h : x ∈ closure s), p x h

Tactic:
simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
⊢ ∀ (h : x ∈ Submonoid.closure (s ∪ s⁻¹)), p x ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : ι
⊢ x✝ = (Equiv.symm σ) (σ x✝)

Tactic:
Equiv.symm_apply_apply

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
x✝ : ι
⊢ x✝ = x✝
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj ↑h • P ≤ H

Tactic:
by
  rintro - ⟨g, hg, rfl⟩
  exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ MulAut.conj h • H

Tactic:
subset_pointwise_smul_iff,

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ (MulAut.conj h)⁻¹ • H ≤ H
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
by
  induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp [ih]

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

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid fun x y ↦ r x y ∨ s x y

Tactic:
rw [eqvGen_eq]

Goal state after:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun x y ↦ ∃ r ∈ S, r x y

Tactic:
rw [eqvGen_eq]

Goal state after:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : Setoid α
⊢ EqvGen.setoid ⇑r ≤ r

Tactic:
rw [eqvGen_eq]

Goal state after:
α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ EqvGen.setoid r ≤ s

Tactic:
rw [eqvGen_eq]

Goal state after:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

Tactic:
rw [nil_append, nil_append, cons.sizeOf_spec, cons.sizeOf_spec]

Goal state after:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + sizeOf (x, b) + (1 + sizeOf (x, !b) + sizeOf L2)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + sizeOf (x, b) + (1 + sizeOf (x, !b) + sizeOf L2)

Tactic:
lia

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a⁻¹ * a = 1

Tactic:
by
    rintro ⟨L⟩
    exact
      List.recOn L rfl fun ⟨x, b⟩ tl ih =>
          Eq.trans (Quot.sound <| by simp [invRev]) ih

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

Goal state before:
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 b

Tactic:
apply prod_eq_single_of_mem b 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
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ (QuotientGroup.con c.subgroup) x y ↔ c x y

Tactic:
rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ c (x⁻¹ * y) 1 ↔ c x y
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ + y₂) * of L3 = x * ((y₁ + y₂) * of L3)

Tactic:
rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ x * y * -of L3 = x * (y * -of L3)

Tactic:
rw [mul_neg, mul_neg, mul_neg, ih]

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

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
· rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
⊢ ↑(u * s₂) ∈ S

Tactic:
exact SetLike.coe_mem (u * s₂)

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 ↑y * f.mk' x y = f x

Tactic:
by rw [mul_comm, mk'_spec]

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 y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z

Tactic:
cases x with | _ r₁ s₁
  cases y with | _ r₂ s₂
  cases z with | _ r₃ s₃
  rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
  rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩; rw [hb']; clear hb'
  rcases oreCondition ra sb with ⟨rc, sc, hc⟩
  rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]; swap
  · rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]
  rw [← mul_assoc, mul_smul]
  symm; apply oreDiv_smul_char
  rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ ((monoidOf S).mk' a b).liftOn f H = f a b

Tactic:
← mk_eq_monoidOf_mk',

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ (mk a b).liftOn f H = f a b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f H = f a b c d

Tactic:
← mk_eq_monoidOf_mk',

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ (mk a b).liftOn₂ (mk c d) f H = f a b c d
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ * b = ⊤

Tactic:
by rw [top_mul', if_neg hb]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (0 * b) = untopD 0 0 * untopD 0 b

Tactic:
zero_mul,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 0 = untopD 0 0 * untopD 0 b
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ ↑(fS (sa * s₁))⁻¹ * f (ra * r₂) = ↑(fS s₁)⁻¹ * f r₁ * (↑(fS s₂)⁻¹ * f r₂)

Tactic:
Units.inv_mul_eq_iff_eq_mul,

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f (ra * r₂) = ↑(fS (sa * s₁)) * (↑(fS s₁)⁻¹ * f r₁ * (↑(fS s₂)⁻¹ * f r₂))
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R

Tactic:
ext
  simp

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

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ↑z = ↑z - ↑0

Tactic:
lia

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

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
key : z < n * (z / n + 1)
⊢ -↑z = ↑((z / n + 1) * n - z) - ↑((z / n + 1) * n)

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ r • m • x = m • r • x

Tactic:
rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x

Tactic:
apply hf.seq_le_seq n <;>
    aesop (add simp [iterate_succ']) (erase simp [iterate_succ])

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (0 * b) = unbotD 0 0 * unbotD 0 b

Tactic:
zero_mul,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 0 = unbotD 0 0 * unbotD 0 b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b

Tactic:
rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : NeZero 1
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
⊢ 1 ≤ x ↔ x ≠ 0

Tactic:
rw [Order.one_le_iff_pos, pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α) a)
a : α
⊢ f ((equivShrink α).symm ((equivShrink α) a)) ≍ f a

Tactic:
Equiv.symm_apply_apply

Goal state after:
α : Type u_1
inst✝ : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α) a)
a : α
⊢ f a ≍ f a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Tactic:
by
  refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))
  apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]

Goal state after:
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Finite (Set α)

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)
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 : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ ↑i + 1 < n

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
by simp [coe_fill, coe_replicate, this]

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

Goal state before:
pp: case isTrue
α : 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
h✝ : ↑i ≤ n
⊢ n + 1 = n + 1

Tactic:
lia

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

Goal state before:
pp: case isFalse
α : 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
h✝ : ¬↑i ≤ n
⊢ n = n + 1

Tactic:
lia

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

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

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a : α
⊢ f a = g a

Tactic:
refine IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ s x (f b) ↔ s x (g b)
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
simp [h, toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
simp [h, toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
simp [h, toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
simp [h, toOption]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' Ici x ⊆ Ici x

Tactic:
rintro _ ⟨y, hy, rfl⟩
    exact le_trans hy (le_map _)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u_4
f : Part α✝
⊢ id <$> f = f

Tactic:
by cases f; rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
· exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s✝
a : Set α
ha : a ∈ s✝
⊢ a ⊆ c₂

Tactic:
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [← hc] at hda

Goal state after:
case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c ↦ Set.range ⇑c) c) a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
⊢ IsChain r c

Tactic:
by
  induction hc with
  | succ _ h => exact h.succ
  | union hs h =>
    exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq

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:
by simp_rw [HPow.hPow, Pow.pow]; rw [cast_succ, power_add, power_one]

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

Goal state before:
pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1

Tactic:
apply zero_le

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
obtain h_a := Eq.le h_a

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a✝ : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
h_a : f a ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀

Tactic:
← one_mul b

Goal state after:
case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2
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✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

Tactic:
funext; congr; ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl

Goal state after: