mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
s : Finset α
hs : ↑s ⊆ ⋃ i, f i
⊢ ∃ i, ↑s ⊆ f i

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ sInf (range fun i ↦ ↑i) = sInf s

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ sInf s = sInf s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
rw [Finset.iSup_insert]
  grind

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi a = {b}
⊢ IsTop b ∧ a ⋖ b

Tactic:
by
    simp_rw [Set.ext_iff, mem_Ioi, mem_singleton_iff] at h
    have hb : a < b := (h b).mpr rfl
    exact ⟨fun c ↦ not_lt.mp fun hc ↦ hc.ne.symm ((h c).mp (hb.trans hc)),
      ⟨hb, fun c hac hcb ↦ hcb.ne ((h c).mp hac)⟩⟩

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

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic 0)

Tactic:
rw [← Nat.bot_eq_zero]

Goal state after:
a b c : ℕ
⊢ Unique ↥(Iic ⊥)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
by
  simpa [← coe_subset] using Set.Ico_subset_Ico ha hb

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f

Tactic:
simp [IsBadSeq]

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

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ ↑(Subgroup.center G)

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ Subgroup.center G
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
n : ℕ
⊢ (ofLex f (g n)).2 ∈ {y | toLex ((ofLex f (g n)).1, y) ∈ s}

Tactic:
simpa using! hf _

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : ConjAct.ofConjAct ↑u * x = x * ConjAct.ofConjAct ↑u
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x

Tactic:
Units.ext_iff,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)
this : ↑(ConjAct.ofConjAct ↑u * x) = ↑(x * ConjAct.ofConjAct ↑u)
⊢ ↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ closure S
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T

Tactic:
by
  simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ comap f (r.map f) = r

Tactic:
apply le_antisymm _ le_comap_map

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ comap f (r.map f) ≤ r
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr.inl
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

Tactic:
exact Step.cons h

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

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
rintro Hyx Hyx' -

Goal state after:
case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
Hyx : ↑y * ↑x = 1
Hyx' : ↑y' * ↑x' = 1
⊢ f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
Hyx : ↑y * ↑x = 1
Hyx' : ↑y' * ↑x' = 1
⊢ f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
⊢ (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

Tactic:
← prod_union sdiff_disjoint,

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁ ∪ s₁, f x = ∏ x ∈ s₂, f x
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((rightRel s) x y)

Tactic:
rightRel_eq

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((fun x y ↦ y * x⁻¹ ∈ s) x y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Tactic:
by rw [union_comm, prod_union_eq_left hs]

Goal state after:
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)
x : FreeGroup α
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
⊢ f x = g x

Tactic:
induction x

Goal state after:
case C1
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
⊢ f 1 = g 1

case of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
⊢ f (of x✝) = g (of x✝)

case inv_of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
a✝ : f (of x✝) = g (of x✝)
⊢ f (of x✝)⁻¹ = g (of x✝)⁻¹

case mul
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ y✝ : FreeGroup α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: β : Type v
inst✝ : Group β
s : Set β
⊢ Subgroup.closure s = Subgroup.closure (Set.range Subtype.val)

Tactic:
Subtype.range_coe

Goal state after:
β : Type v
inst✝ : Group β
s : Set β
⊢ Subgroup.closure s = Subgroup.closure s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℤ
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) x) = x

Tactic:
induction x

Goal state after:
case zero
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) 0) = 0

case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) ↑i✝) = ↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (↑i✝ + 1)) = ↑i✝ + 1

case pred
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝)) = -↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝ - 1)) = -↑i✝ - 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
x✝ : x ∈ s
hx : x ∉ m
⊢ x ^ count x m = 1

Tactic:
count_eq_zero_of_not_mem hx,

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
x : M
x✝ : x ∈ s
hx : x ∉ m
⊢ x ^ 0 = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : Multiset M
s : Finset M
l : List M
⊢ Multiset.toFinset (Quot.mk (⇑(isSetoid M)) l) ⊆ s →
    Multiset.prod (Quot.mk (⇑(isSetoid M)) l) = ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid M)) l)

Tactic:
simp only [quot_mk_to_coe'', prod_coe, coe_count]

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : Multiset M
s : Finset M
l : List M
⊢ (↑l).toFinset ⊆ s → l.prod = ∏ x ∈ s, x ^ List.count x l
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ {x, g x hx} ⊆ s

Tactic:
simp [insert_subset_iff, hx, g_mem]

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✝ : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default

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

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

Goal state before:
pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
· simp [s]

Goal state after:
case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
· simp [s]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
inst✝ : Mul α
x y : α
⊢ of x * of y = of (x * y)

Tactic:
rw [mul_def, lift_apply_of, lift_apply_of]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅p, q⁆ ∈ ↑N

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅p, q⁆ ∈ N
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
p : Localization S → Sort u
f : (a : M) → (b : ↥S) → p (mk a b)
H : ∀ {a c : M} {b d : ↥S} (h : (r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d
x : Localization S
y z : M × ↥S
h : (OreLocalization.oreEqv S M) y z
⊢ ⋯ ▸ f y.1 y.2 = f z.1 z.2

Tactic:
by cases y; cases z; exact H (r_iff_oreEqv_r.mpr h)

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ (∀ (x y : M), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)

Tactic:
intro H z w h
    obtain ⟨_, _⟩ := f.surj z
    obtain ⟨_, _⟩ := f.surj w
    rw [← f.mk'_sec z, ← f.mk'_sec w]
    exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
lift a₁ to α using ha.lt_top.ne

Goal state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₁ b₂ : WithTop α
hb : b₁ < b₂
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
⊢ ↑a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ ↑x * a < ↑x * ⊥

Tactic:
exact absurd h not_lt_bot

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

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ a * ↑x < ⊥ * ↑x

Tactic:
exact absurd h not_lt_bot

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
⊢ sInf (Ioi ⊤) ≤ succ ⊤

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
ha : a ≠ ⊤
⊢ sInf (Ioi a) ≤ succ a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < succ y
⊢ x ≤ y

Tactic:
exact le_of_lt_succ h

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : α
h✝ : ¬succ a = a
⊢ Option.some a ≤ ↑(succ a)

Tactic:
exact coe_le_coe.2 (le_succ a)

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

Goal state before:
pp: case top.coe
a✝ : ℕ
⊢ (⊤ * ↑a✝).toNat = ⊤.toNat * (↑a✝).toNat

Tactic:
rename_i b; cases b <;> simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
by_cases hs : i ∈ s
  · convert! (s.prod_inter_mul_prod_sdiff { i } f).symm
    simp [hs]
  · simp_all only [not_false_eq_true, forall_const, one_mul]
    apply Finset.prod_congr <;> aesop

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (f 0 ::ᵥ ofFn fun i ↦ f i.succ).toList = List.ofFn f

Tactic:
List.ofFn_succ,

Goal state after:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (f 0 ::ᵥ ofFn fun i ↦ f i.succ).toList = f 0 :: List.ofFn fun i ↦ f i.succ
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 : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ ∀ (x : α), x ∈ v.toList → p x

Tactic:
by
        simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
        exact hp.2

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head ∈ v.toList

Tactic:
by
      rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]; exact .inl rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).head = f 0

Tactic:
← get_zero,

Goal state after:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).get 0 = f 0
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.head = v.last

Tactic:
← get_zero,

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.get 0 = v.last
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (↑m).card = countP (fun x ↦ a = x) ↑m + countP (fun x ↦ ¬a = x) ↑m

Tactic:
← card_eq_countP_add_countP _ _

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (↑m).card = (↑m).card
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.cons.cons
α : 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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨b :: v, v_property⟩ w

Tactic:
rcases w with ⟨_ | ⟨c, w⟩, w_property⟩

Goal state after:
case succ.cons.cons.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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
w_property : [].length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨b :: v, v_property⟩ ⟨[], w_property⟩

case succ.cons.cons.cons
α : 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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
c : γ
w : List γ
w_property : (c :: w).length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨b :: v, v_property⟩ ⟨c :: w, w_property⟩
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
Option.mem_def

Goal state after:
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range Subtype.val

Tactic:
Subtype.range_coe

Goal state after:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α β : Type u_6
f : α → β
x : List α
⊢ traverseAux (pure ∘ f) x = pure ⟨List.map f x, ⋯⟩

Tactic:
induction x

Goal state after:
case nil
α β : Type u_6
f : α → β
⊢ traverseAux (pure ∘ f) [] = pure ⟨List.map f [], ⋯⟩

case cons
α β : Type u_6
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : traverseAux (pure ∘ f) tail✝ = pure ⟨List.map f tail✝, ⋯⟩
⊢ traverseAux (pure ∘ f) (head✝ :: tail✝) = pure ⟨List.map f (head✝ :: tail✝), ⋯⟩
Module: Mathlib.Data.Sum.Order

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

Tactic:
refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
hab : a < b
⊢ ¬b ≤ a

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