mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ l' ∈ map (cons a) (sublistsLen n l)
⊢ l'.length = n + 1

Tactic:
mem_map

Goal state after:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ l'.length = n + 1
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
rw [sup_eq_left.mpr ha]
        apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ x ∈ map (Embedding.sigmaMk ⟨x.1, b⟩.fst) (f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd)

Tactic:
mem_map

Goal state after:
case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ ∃ a_1 ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd, (Embedding.sigmaMk ⟨x.1, b⟩.fst) a_1 = x
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ map (Embedding.sigmaMk ⟨i, b⟩.fst) (f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd) ↔ x ∈ f a b

Tactic:
mem_map

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x

Tactic:
iff_comm,

Goal state after:
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Q x ∧ Minimal P x ↔ Minimal (fun x ↦ Q x ∧ P x) x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioo a a = 0

Tactic:
rw [Ioo, Finset.Ioo_self, Finset.empty_val]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hbc : b ≤ c
⊢ {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a b).val

Tactic:
Finset.Ico_filter_lt_of_right_le hbc

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hbc : b ≤ c
⊢ (Finset.Ico a b).val = (Finset.Ico a b).val
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ (Finset.Ico a b).val ∩ (Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val

Tactic:
← Finset.inter_val,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ (Finset.Ico a b ∩ Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅

Tactic:
simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ico]

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), x n ∈ s
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Ioi_self

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)

Tactic:
by rw [inv_smul_smul]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
⊢ hs.min ⋯ = a

Tactic:
by_contra h

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min ⋯ = a
⊢ False
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ z * a * c = a * c * z

Tactic:
← h.left_assoc,

Goal state after:
M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ z * (a * c) = a * c * z
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * (z * c)

Tactic:
rw [h.comm, ← h.right_assoc, ← h.comm, ← h.left_assoc, h.comm]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : M
⊢ Commute 1 x✝

Tactic:
by rw [commute_iff_eq, one_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * 1 = x✝¹ * (x✝ * 1)

Tactic:
by rw [mul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : MulOneClass M
⊢ 1 ∈ S.centralizer

Tactic:
by simp [mem_centralizer_iff]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case e'_5
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩

Tactic:
exact PSigma.subtype_ext (Subtype.ext h') rfl

Goal state after:
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 ⋯
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 ⋯

Tactic:
induction h using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left x hx y hy ih =>
    cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
⊢ (⨆ i ∈ s, H i).Normal

Tactic:
by
  rw [← iSup_subtype'']
  have : ∀ i : s, (H i).Normal := fun i ↦ h i i.property
  apply iSup_normal

Goal state after:
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:
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.Data.Finset.NoncommProd

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ i = x i

Tactic:
apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans

Goal state after:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 ↦ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

case a
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i))
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : c x y
⊢ d ↑x ↑y

Tactic:
c.eq.2 h

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : c x y
⊢ d ↑y ↑y
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ : M →* P
f : c.Quotient →* P
x y : M
h : c x y
⊢ f ↑x = f ↑y

Tactic:
c.eq.2 h

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ : M →* P
f : c.Quotient →* P
x y : M
h : c x y
⊢ f ↑y = f ↑y
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
⊢ mk ⁻¹' mk '' s = ↑N * s

Tactic:
ext a
  constructor
  · rintro ⟨b, hb, h⟩
    refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
    simp only [h, QuotientGroup.mk_div, div_self']
  · rintro ⟨a, ha, b, hb, rfl⟩
    refine ⟨b, hb, ?_⟩
    simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
exact card_union_le ..

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hle : ⁅⊤, H⁆ ≤ H
h : G
hh : h ∈ H
g : G
⊢ g * h * g⁻¹ ∈ H

Tactic:
exact (H.mul_mem_cancel_right <| H.inv_mem hh).mp <| commutator_le.mp hle g trivial h hh

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) → ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
· rintro ⟨u, hu, e⟩
    exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ 1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)

Tactic:
by
  simp [oreDiv_mul_char 1 r t 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
P : Type u_3
inst✝ : CommMonoid P
z : Localization S
x : M × ↥S
⊢ mk (↑x.2 * x.1) (x.2 * 1) = mk x.1 1

Tactic:
← mk_mul,

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
z : Localization S
x : M × ↥S
⊢ mk (↑x.2) x.2 * mk x.1 1 = mk x.1 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ (r s) (a₁, a₂) (b₁, b₂) ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
r_iff_exists,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ (∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)) ↔ ↑b₂ * a₁ = ↑a₂ * b₁
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr.coe.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
⊢ ↑a * ↑b * c = ↑a * (↑b * c)

Tactic:
| coe b =>

Goal state after:
case inr.inr.inr.coe.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
⊢ ↑a * ↑b * c = ↑a * (↑b * c)
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:
by
    rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]

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

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

Tactic:
exact mul_le_mul_of_nonneg_right h x0

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

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

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

Tactic:
· exact (hb <| hba.trans <| le_succ _).trans (le_succ _)

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b

Tactic:
by_cases h : IsMax a
  · rwa [h.succ_eq]
  · rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
    refine ⟨ha, fun hab => ?_⟩
    subst hab
    exact (h hb.isMax).elim

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = ⨅ b, ⨅ (_ : b > a), b

Tactic:
iInf_subtype',

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = ⨅ x, ↑x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
⊢ ¬a + 1 = 0

Tactic:
by_contra h

Goal state after:
case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
h : a + 1 = 0
⊢ False
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default

Tactic:
rwa [this.1, Nat.cast_one, Units.val_eq_one] at x_y

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

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
x✝ : ι
a✝ : x✝ ∈ s
⊢ f = t.piecewise f f

Tactic:
simp +unfoldPartialApp [Finset.piecewise]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.get (Fin.last n)

Tactic:
get_eq_get_toList

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝

Tactic:
simp only [elim_inl, lex_inr_inr, coe_le_coe]

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inl
α : 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 : α
hyz : y ≠ z
hsz : sy ∈ cs
hzsz : z ∈ sy
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsy).right hysy hzsz hyz

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
constructor <;> introv h
  · apply h
  · apply le_trans _ (h (max i j))
    trans c₀ i (c₁ (max i j))
    · apply (c₀ i).monotone
      apply c₁.monotone
      apply le_max_right
    · apply c₀.monotone
      apply le_max_left

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

Goal state before:
pp: case mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ

Tactic:
let ⟨a⟩ := mk_ne_zero_iff.1 hα

Goal state after:
case mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: n : ℕ∞
x : Cardinal.{u_1}
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

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

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

Tactic:
by_contra h

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ c
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
by
  rw [lift_iSup hf]
  exact ciSup_le' w

Goal state after:
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:
rw [← one_mul b]
      exact (mul_le_mul' ha le_rfl).trans_lt h

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ℵ₀ * ↑n = ℵ₀

Tactic:
rw [mul_comm, nat_mul_aleph0 hn]

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

Goal state before:
pp: c : Cardinal.{u_1}
n : ℕ
h : c ≤ ↑n
⊢ ∃ m ≤ n, c = ↑m

Tactic:
lift c to ℕ using h.trans_lt natCast_lt_aleph0

Goal state after:
n c : ℕ
h : ↑c ≤ ↑n
⊢ ∃ m ≤ n, ↑c = ↑m
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ n = m

Tactic:
replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
n m : ℕ
x : M
hx : x ≠ 0
h : ↑n • x = ↑m • x
⊢ n = m
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
rintro ⟨_, x, _⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← one_smul N a]); rfl
    congr 1
    · funext i; congr; ext m a; clear i; (conv_rhs => rw [← one_smul N a]); rfl
    · ext n a; (conv_rhs => rw [← one_smul M (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..

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

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x + -y ∈ p ↔ x ∈ p

Tactic:
p.add_mem_iff_left (p.neg_mem hy)

Goal state after:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x ∈ p ↔ x ∈ p
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
p : Submodule R M
⊢ ↑p = Set.univ ↔ p = ⊤

Tactic:
iff_comm,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊤ ↔ ↑p = Set.univ