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

Goal state before:
pp: case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩

Goal state after:
case tail.inr
α : Type u
L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')
h₂ : Red w₂ L₂
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
h₁

Goal state after:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]
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
p : ι → Prop
inst✝ : DecidablePred p
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x

Tactic:
have := prod_map (s.subtype p) (Function.Embedding.subtype _) f

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
this : ∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x = ∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p) x)
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤

Tactic:
by rw [Finset.coe_univ]; exact Submonoid.closure_univ

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
n : ℕ
f : ℕ → M
⊢ ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k

Tactic:
by
  induction n with
  | zero => rw [prod_range_one, prod_range_one]
  | succ n ih =>
    rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
    simp [← ih]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
fg_iff_submonoid_fg

Goal state after:
G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG

Tactic:
fg_iff_submonoid_fg

Goal state after:
ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G)) G' = G'
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

Tactic:
ext ⟨x⟩

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G)) G' = G'
x✝ : G ⧸ G'
x : G
⊢ (congr G' G' (MulEquiv.refl G) he) (Quot.mk (⇑(leftRel G')) x) = (MulEquiv.refl (G ⧸ G')) (Quot.mk (⇑(leftRel G')) x)
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
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
xbar : Quotient R
xbar_in_s : xbar ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ s with ⟦y⟧ = xbar, f y = 1

Tactic:
obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
x : ι
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
⊢ p ∈ H₁ → ∀ g₂ ∈ H₂, ⁅f p, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
hp

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
⊢ ∀ g₂ ∈ H₂, ⁅f p, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (of default)) = of default

Tactic:
simp only [one_smul, lift_apply_of]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ f 0 ≤ f a

Tactic:
exact OrderHomClass.mono _ ha

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ f 0

Tactic:
exact OrderHomClass.mono _ ha

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

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
v : P
y : ↥S
⊢ (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v

Tactic:
rw [f.lift_mk' hg]; exact mul_inv_left hg _ _ _

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂)) = rc • rb • r₃ /ₒ (sc * sa * s₁)

Tactic:
apply oreDiv_smul_char

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑(sc * sa) * r₁ = rc * ↑(sb * s₂)
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
m : M
hm : IsRegular m
⊢ IsRegular (f m)

Tactic:
refine (Commute.isRegular_iff (Commute.all _)).mpr fun n₁ n₂ eq ↦ ?_
  have ⟨ms₁, eq₁⟩ := f.surj n₁
  have ⟨ms₂, eq₂⟩ := f.surj n₂
  rw [← (f.map_units (ms₁.2 * ms₂.2)).mul_left_inj, Submonoid.coe_mul]
  replace eq := congr($eq * f (ms₁.2 * ms₂.2))
  simp_rw [mul_assoc] at eq
  rw [map_mul, ← mul_assoc n₁, eq₁, ← mul_assoc n₂, mul_right_comm n₂, eq₂] at eq ⊢
  simp_rw [← map_mul, eq_iff_exists] at eq ⊢
  simp_rw [mul_left_comm _ m] at eq
  exact eq.imp fun _ ↦ (hm.1 ·)

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

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b

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

Tactic:
· simp_rw [mul_bot x0', bot_le]

Goal state after:
case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ b
⊢ ↑x * ↑a✝ ≤ ↑x * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a < (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a < b

Tactic:
simp only at h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a < (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a < b

Tactic:
simp only at h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a ≤ (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a ≤ b

Tactic:
simp only at h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : x * a ≤ x * b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a ≤ (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a ≤ b

Tactic:
simp only at h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a * x ≤ b * x
⊢ a ≤ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬¬IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
not_not

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ : SuccOrder α
⊢ ∀ (b : SuccOrder α), h₀ = b

Tactic:
h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
⊢ h₀ = h₁
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n - 0] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
Nat.sub_zero

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 0] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n - 0] i)

Tactic:
Nat.sub_zero

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n] i)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
h : ⊤ < ↑a✝
⊢ (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝

Tactic:
exact (not_top_lt h).elim

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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha :
  ⊤ ≤
    match ⊤ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ⊤

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha :
  ↑a✝ ≤
    match ↑a✝ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ↑a✝

Tactic:
· exact ((coe_lt_top (⊤ : α)).not_ge ha).elim

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha :
  ↑a✝ ≤
    match ↑a✝ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ x + n

Tactic:
exact add_left_injective_of_ne_top hn

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

Goal state before:
pp: case neg.inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
· simp [h]

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

Goal state before:
pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
· simp [h]

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

Goal state before:
pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
· simp [h]

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 ι
a : ι
b : (x : ι) → x = a → M
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1

Tactic:
by
  split_ifs with h
  · rw [Finset.prod_eq_single a, dif_pos rfl]
    · intro _ _ h
      rw [dif_neg]
      exact h
    · simp [h]
  · rw [Finset.prod_eq_one]
    grind

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (x : α ⊕ β), x ∈ univ.disjSum univ

Tactic:
rintro (_ | _)

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ univ.disjSum univ

case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ univ.disjSum univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
i : ι
hi : i ∈ s
hpi : p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
rw [prod_eq_single_of_mem _ hi, if_pos hpi]

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
i : ι
hi : i ∈ s
hpi : p i
⊢ ∀ b ∈ s, b ≠ i → (if p b then a else 1) = 1
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Set α
⊢ s ∈ map coeEmb.toEmbedding Finset.univ

Tactic:
by
    classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp

Goal state after:
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 α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (n + 1).pred = n

Tactic:
Nat.add_one,

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ n.succ.pred = n
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ x.tail.get i = x.get ⟨↑i + 1, ⋯⟩

Tactic:
by
  obtain ⟨i, ih⟩ := i; dsimp
  rcases x with ⟨_ | _, h⟩ <;> try rfl
  rw [List.length] at h
  rw [← h] at ih
  contradiction

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s

pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ n, s n = ⊤
⊢ sSup (range s) = ⊤

Tactic:
rwa [sSup_range]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
have heq : a.1 = b.1 := Subsingleton.allEq _ _
    simp [Prod.Lex.toLex_le_toLex, heq]

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

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

Tactic:
not_not

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : IsMin (sSup s) ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ ((a : ι) → Quotient.out #(f a) → ULift α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine Equiv.piCongrRight fun b => ?_

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ (Quotient.out #(f b) → ULift α) ≃ Quotient.out #(f b → α)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inl a ≤ inl b

Tactic:
change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
        simp [toDual_le_toDual, inl_le_inl_iff]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
⊢ (p₁, p₂) ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x} → (fun x ↦ (f x, g x)) a ≤ (p₁, p₂)

Tactic:
hp

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : (p₁, p₂) ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}
⊢ (fun x ↦ (f x, g x)) a ≤ (p₁, p₂)
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
o : Part α
⊢ ¬¬o.Dom → ∃ x, o = some x

Tactic:
not_not

Goal state after:
case mp
α : Type u_1
o : Part α
⊢ o.Dom → ∃ x, o = some x
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
⊢ b' ∈ y → b' ∈ x

Tactic:
h₁

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
⊢ o.bind f = f (o.get h)

Tactic:
by
  ext b
  simp only [Part.mem_bind_iff]
  refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
  rintro ⟨a, ha, hb⟩
  rwa [Part.get_eq_of_mem ha]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
ext n : 2

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n
Module: Mathlib.Order.CompleteLattice.Chain

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

Tactic:
h₁

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
⊢ ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ 0 ^ c ≤ 1

Tactic:
by_cases h : c = 0
  · rw [h, power_zero]
  · rw [zero_power h]
    apply zero_le

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ IsSuccLimit c

Tactic:
rw [Cardinal.isSuccLimit_iff]
  exact ⟨hc.ne_zero, hc.isStrongPrelimit.isSuccPrelimit⟩

Goal state after: