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

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i

Tactic:
· simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup ↑s

Tactic:
rw [sup'_eq_csSup_image s hs, Set.image_id]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : IsEmpty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
simp [map_bot]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⩿ ⊤ ↔ IsMax a

Tactic:
simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
⊢ s.Infinite

Tactic:
inhabit α
  let f (n : ℕ) : α := Nat.recOn n (h default).choose fun _ a ↦ (h a).choose
  have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
  exact infinite_of_injective_forall_mem
    (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
this : IsTop a
⊢ {a}.Subsingleton ∧ IsCofinal {a}

Tactic:
by simpa [IsCofinal]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
⊢ Minimal (fun x ↦ x ∈ f '' s) (f x)

Tactic:
refine ⟨mem_image_of_mem f hx.prop, ?_⟩
  rintro _ ⟨y, hy, rfl⟩
  rw [hf hx.prop hy, hf hy hx.prop]
  exact hx.le_of_le hy

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
hca : c ≤ a
⊢ filter (fun x ↦ x < c) (Ico a b) = ∅

Tactic:
by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (insert a (Finset.Ioo a b)).val = Ico a b

Tactic:
Finset.Ioo_insert_left h

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c

Tactic:
rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]

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

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

Tactic:
Finset.Ico_inter_Ico

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

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1

Tactic:
rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]

Goal state after:
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s

Tactic:
exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective

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

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ∀ (n : ℕ), (∀ m ≥ n + 1, P m) → ∀ m ≥ n, P m

pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}

Tactic:
· intro n ih m hm
    rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
⊢ ∀ (a : { x // x ∈ range f }), Acc (Subrel r fun x ↦ x ∈ range f) a

Tactic:
rintro ⟨_, c, rfl⟩

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (Subrel r fun x ↦ x ∈ range f) ⟨f c, ⋯⟩
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

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

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
h : TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
⊢ x < y
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ↑a ∈ center M
⊢ ↑a⁻¹ ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *
  exact (Commute.units_inv_right <| ha ·)

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

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ ofAdd s.sum = (List.map (⇑ofAdd) s).prod

Tactic:
simp [ofAdd]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ (Multiset.map Subtype.val m).prod ∈ S

Tactic:
rw [← coe_multiset_prod]

Goal state after:
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ ofAdd s.sum = (Multiset.map (⇑ofAdd) s).prod

Tactic:
simp [ofAdd]; rfl

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

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
x y : α
⊢ (∃ r ∈ s, r x y) ↔ (⨆ a ∈ s, ⇑a) x y

Tactic:
simp only [iSup_apply, iSup_Prop_eq, exists_prop]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x

Tactic:
refine Eq.trans ?_ (fold_disjiUnion h)

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x =
    fold (fun x1 x2 ↦ x1 * x2) (fold (fun x1 x2 ↦ x1 * x2) 1 (fun i ↦ 1) s) (fun x ↦ f x) (s.disjiUnion t h)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂

Tactic:
simpa only [invRev_invRev] using h.invRev

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂

Tactic:
simpa only [invRev_invRev] using h.invRev

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk (L ++ (List.replicate n L).flatten) = mk (L :: List.replicate n L).flatten

Tactic:
List.flatten_cons

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk (L ++ (List.replicate n L).flatten) = mk (L ++ (List.replicate n L).flatten)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ (lift f).range ≤ s

Tactic:
rintro _ ⟨⟨L⟩, rfl⟩
  exact List.recOn L s.one_mem fun ⟨x, b⟩ tl ih ↦
    Bool.recOn b (by simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
      (by simpa using s.mul_mem (H ⟨x, rfl⟩) ih)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
F : Fintype (Subtype p)
s : Finset ι
h : ∀ (x : ι), x ∈ s ↔ p x
f : ι → M
⊢ ∏ a ∈ s, f a = ∏ a, f ↑a

Tactic:
obtain rfl : p = (· ∈ s) := by simp [h]
  rw [← prod_coe_sort]
  congr!

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Group G
inst✝³ : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x : G ⧸ N
⊢ (map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x

Tactic:
refine induction_on x fun x => ?_
  simp only [map_mk, MonoidHom.comp_apply]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
⊢ FG G → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
rw [fg_iff_exists_freeGroup_hom_surjective]

Goal state after:
case mp
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
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 ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b

Tactic:
· exact False.elim (card_ne_zero_of_mem hx hc0)

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b
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 : ι
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
exact hp

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

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = n * ↑s

Tactic:
mul_comm (s : R) m,

Goal state after:
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ m * ↑s = n * ↑s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default

Tactic:
rw [h.eq_singleton_default, Finset.prod_singleton]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ = ⊥ ↔ H ≤ center G

Tactic:
commutator_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, ⊤⁆ = ⊥ ↔ H ≤ center G
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ (closure base).Normal

Tactic:
rw [h_base]
    exact Subgroup.normalClosure_normal

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z : FreeAbelianGroup α
⊢ x * y * z = x * (y * z)

Tactic:
induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]

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

Goal state before:
pp: case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ mk ↑y✝.2 ⟨y✝.1, ⋯⟩ * mk y✝.1 y✝.2 = 1

Tactic:
mk_eq_monoidOf_mk',

Goal state after:
case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ (monoidOf ⊤).mk' ↑y✝.2 ⟨y✝.1, ⋯⟩ * (monoidOf ⊤).mk' y✝.1 y✝.2 = 1
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b

Tactic:
· rw [← sub_add_cancel b a, map_add f]
    exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f.symm a ≤ f.symm b

Tactic:
rw [← map_le_map_iff f]
    convert! Iff.rfl <;>
    exact f.toEquiv.apply_symm_apply _

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
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑t₂ * (↑d.2 * c.1) * (↑t₁ * (↑b.2 * a.1)) = ↑t₂ * ↑t₁ * (↑a.2 * ↑c.2 * (b.1 * d.1))

Tactic:
ht₁,

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
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑t₂ * (↑d.2 * c.1) * (↑t₁ * (↑a.2 * b.1)) = ↑t₂ * ↑t₁ * (↑a.2 * ↑c.2 * (b.1 * d.1))
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
induction a <;> induction b <;>
    simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : Subsingleton M
x y : N
⊢ x = y

Tactic:
by
    obtain ⟨mx, sx, rfl⟩ := f.mk'_surjective x
    obtain ⟨my, sy, rfl⟩ := f.mk'_surjective y
    exact congr(f.mk' $(Subsingleton.elim ..) $(Subsingleton.elim ..))

Goal state after:
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
⊢ a < succ b

Tactic:
apply lt_succ_of_le_of_not_isMax h hb

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k + 1] b = a

Tactic:
iterate_add_apply,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k] (pred^[1] b) = a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
by_cases hm' : m ∈ S

Goal state after:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ x, IsGreatest S x

case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
⊢ n < 2 ↔ n ≤ 1

Tactic:
rw [← one_add_one_eq_two, lt_add_one_iff one_ne_top]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
⊢ StrictMonoOn f s

Tactic:
rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le
  obtain _ | n := n
  · simp at hab
  apply not_isMin_of_lt at hab
  induction n with
  | zero => simpa using hf _ hab hb ha
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n + 1] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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

Goal state before:
pp: case zero.nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C ⟨[], ⋯⟩

Tactic:
exact nil

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

Goal state before:
pp: case zero.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩

Tactic:
exact nil

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

Goal state before:
pp: case zero.nil.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩ ⟨[], ⋯⟩

Tactic:
exact nil

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx (i + 1) =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

Tactic:
← List.insertIdx_eraseIdx_of_le

Goal state after:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬LiftRel r s a a

Tactic:
by rintro _ (⟨h⟩ | ⟨h⟩) <;> exact irrefl _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬Lex r s a a

Tactic:
by rintro _ (⟨h⟩ | ⟨h⟩) <;> exact irrefl _ h

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
b : α ⊕ β
⊢ Sum.Lex r s b ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    b ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part (α✝ → β✝)
y : Part α✝
⊢ (do
        let x ← x
        x <$> y).Dom ↔
    (x <*> y).Dom

Tactic:
simp [(· >>= ·), Part.bind, assert, Seq.seq, (· <$> ·)]

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

Goal state before:
pp: α : 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 : α → β := s.piecewise f g'
⊢ f '' s ∪ (f '' s)ᶜ = univ

Tactic:
union_compl_self

Goal state after:
α : 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 : α → β := s.piecewise f g'
⊢ univ = univ
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c' : Cardinal.{u}
c : ℕ∞
⊢ c ≤ toENat c' ↔ ↑c ≤ c'

Tactic:
enat_gc _

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

Goal state before:
pp: n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀

Tactic:
rw [succ_natCast, ← Nat.cast_add_one]

Goal state after:
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(n + 1) < ℵ₀
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
⊢ r • ↑s = ↑s

Tactic:
apply subset_antisymm (smul_subset_self _ s)

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
⊢ ↑s ⊆ ↑r • ↑s