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

Goal state before:
pp: α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))

Tactic:
rw [← List.append_assoc, ← List.append_assoc]; constructor

Goal state after:
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 : { d // c ≤ d }
⊢ ker c.mkMulHom ≤ ↑d

Tactic:
Con.ker_mkMulHom_eq

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 : { d // c ≤ d }
⊢ c ≤ ↑d
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail
α : Type u
L₁ L₂ b✝ c✝ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b✝
h₂₃ : Step b✝ c✝
ih : ∃ n, L₁.length = b✝.length + 2 * n
⊢ ∃ n, L₁.length = c✝.length + 2 * n

Tactic:
| tail _h₁₂ h₂₃ ih =>

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
c : Con G
a✝ b✝ : G
hx : a✝ ∈ {x | c x 1}
hy : b✝ ∈ {x | c x 1}
⊢ a✝ * b✝ ∈ {x | c x 1}

Tactic:
simpa using c.mul hx hy

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
r : R
s : ↥S
⊢ ↑s * r = r * ↑s

Tactic:
mul_comm

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
r : R
s : ↥S
⊢ r * ↑s = r * ↑s
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 * (↑p)⁻¹ * (↑q)⁻¹ = 1

Tactic:
rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{ toFun := ⇑(lift ⇑((↑F).comp ofMulHom)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } = ↑F

Tactic:
← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{ toFun := ⇑(lift ⇑((↑F).comp ofMulHom)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } =
    lift (lift.symm ↑F)
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
⊢ f x⁻¹ ≤ g x⁻¹ ↔ g x ≤ f x

Tactic:
suffices h : ∀ (f g : F) (x), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x from
    ⟨h f g x, by simpa using h g f x⁻¹⟩
  exact fun f g x hfg ↦ calc
    _ = f x * (f x⁻¹ * g x) := by simp [← mul_assoc, ← map_mul]
    _ ≤ f x * (g x⁻¹ * g x) := by gcongr
    _ = f x                 := by simp [← map_mul]

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
y : ↥S
⊢ f ↑(f.sec (f.mk' x y)).2 * f x = f x * f ↑(f.sec (f.mk' x y)).2

Tactic:
mul_comm

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)
z : N
w v : P
⊢ w * g (f.sec z).1 = g ↑(f.sec z).2 * v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
mul_comm

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ g (f.sec z).1 * w = g ↑(f.sec z).2 * v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
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 : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑c.2 * (↑t₁ * (↑b.2 * a.1)) = ↑t₁ * ↑a.2 * (↑t₂ * (↑c.2 * b.1))

Tactic:
by rw [ht₁]; ac_rfl

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

Tactic:
by
  rw [lift_spec, ← g.map_mul]; exact f.eq_of_eq hg (by rw [sec_spec', map_mul])

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₁ * (↑a.2 * b.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₂ * (↑c.2 * d.1) * (↑t₁ * (↑a.2 * b.1)) = ↑t₂ * ↑t₁ * (↑a.2 * ↑c.2 * (b.1 * d.1))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)
⊢ b (p, q) (x, y)

Tactic:
rw [← one_mul (p, q), ← one_mul (x, y)]
      refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
      convert! b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
      dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
      simp_rw [mul_assoc, ht, mul_comm y q]

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k (g x) = k (g ↑y) * k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
mul_mk'_eq_mk'_of_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
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k (g x) = k.mk' (g ↑y * g x) ⟨g ↑y, ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ * w = z ↔ w = f ↑y * z
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ z * f ↑(f.sec z).2 = f.toMonoidHom ↑(f.sec z).2 * z

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ f ↑(f.sec z).2 * z = f.toMonoidHom ↑(f.sec z).2 * z
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f x * f ↑y = f.toMonoidHom ↑y * f x

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f ↑y * f x = f.toMonoidHom ↑y * f x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y : ↥S
⊢ f x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

Tactic:
mul_mk'_eq_mk'_of_mul

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y : ↥S
⊢ f.mk' (x₁ * x₂) y = f.mk' (x₁ * x₂) y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : MonoidWithZero α
inst✝² : NoZeroDivisors α
inst✝¹ : Nontrivial α
x : WithTop α
n : ℕ
inst✝ : Preorder α
⊢ x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top, pow_ne_top_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ¬IsMax a✝
x✝ : α
⊢ a✝ < x✝ ↔ (if h : (Ioi a✝).Nonempty then ⋯.min (Ioi a✝) h else a✝) ≤ x✝

Tactic:
rw [not_isMax_iff] at ha
      simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]
      exact ⟨wellFounded_lt.min_le (s := Ioi _), lt_of_lt_of_le (wellFounded_lt.prop_min ha)⟩

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
⊢ succ a ≤ succ b

Tactic:
by_cases hba : b ≤ a

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

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: case top
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ IsSuccLimit ⊤ ↔ ⊤ = ⊤ ∨ ∃ y, ⊤ = ↑y ∧ IsSuccLimit y

Tactic:
simp [Order.isSuccLimit_iff, WithTop.exists]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedGT α
inst✝ : SuccOrder α
⊢ IsPredArchimedean αᵒᵈ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ succ x

Tactic:
exact wcovBy_succ x

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑(n + 1)

Tactic:
rw [Nat.cast_add_one, ← sub_sub]
    exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Tactic:
by
  simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

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

Goal state before:
pp: case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : IsEmpty β
⊢ Small.{u, w} β

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
⊢ ∀ (a : PredOrder (WithTop α)), False

Tactic:
intro

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
⊢ False
Module: Mathlib.Data.ENat.Basic

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

Tactic:
by
  simp_rw [add_comm n _]
  exact add_left_injective_of_ne_top hn

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

Goal state before:
pp: c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ c * a

Tactic:
mul_comm

Goal state after:
c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toRight = ∅ ↔ u ⊆ map Function.Embedding.inl univ

Tactic:
by simp [subset_map_inl]

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 : ι
h : i ∈ s
f : ι → M
⊢ f i * ∏ x ∈ s \ {i}, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
mul_comm

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ (∏ x ∈ s \ {i}, f x) * f i = (∏ x ∈ s \ {i}, f x) * f i
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
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

Tactic:
obtain ⟨i, hi, hpi⟩ := h

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
⊢ (∏ i ∈ s, if p i then a else 1) = a
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
left✝ : Finite α
right✝ : Finite β
⊢ Finite (α ⊕ β)

Tactic:
infer_instance

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

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Finite α
val✝ : Fintype α
⊢ Finite (Set α)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty β
h : Uncountable α
⊢ Uncountable (α × β)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty α
h : Uncountable β
⊢ Uncountable (α × β)

Tactic:
infer_instance

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

Goal state before:
pp: case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin 0 → ℕ)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (n - ↑m₂.fst) = ↑m₂.fst

Tactic:
Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)

Goal state after:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ ↑m₂.fst = ↑m₂.fst
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
this : Encodable α
⊢ Countable (List α)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Function.uncurry f '' s ×ˢ t)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(Set.range (Sum.elim Subtype.val Subtype.val))

Tactic:
infer_instance

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

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
intro

Goal state after:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simpa using trans_trichotomous_left ha hb

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : α ⊕ₗ β), inl ⊥ ≤ a

Tactic:
rintro (a | b)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ inl ⊥ ≤ inl a

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : α ⊕ₗ β), a ≤ inr ⊤

Tactic:
rintro (a | b)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ inr ⊤

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ inr ⊤
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : α ⊕ₗ β), a ≤ inr ⊤

Tactic:
rintro (a | b)
    · exact Lex.sep _ _
    · exact Lex.inr le_top

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ (match Sum.inl f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
PrincipalSeg.trans_apply,

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ g.toRelEmbedding (f'.toRelEmbedding a) = g.toRelEmbedding (f a)
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n] (f a₁) ⊔ a₂ = (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
← Function.iterate_succ_apply

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n.succ] a₁ ⊔ a₂ = (⇑f)^[n + 1] a₁ ⊔ a₂
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.fst

Tactic:
intro d hd₁ hd₂ hd₃ a ha
  simp only [isLUB_prod] at ha
  exact ha.1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ f (ωSup₀ c)

Tactic:
rw [h']; apply le_ωSup (c.map f)

Goal state after:
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✝
⊢ ⋃₀ s✝ = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝

Tactic:
apply Or.imp_left h.antisymm'

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✝
⊢ ⋃₀ s✝ ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c

Tactic:
by
  simp only [ωSup, Part.ωSup]
  constructor
  · exact fun a ↦ mem_chain_of_mem_ωSup a
  · intro h
    have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
    rw [dif_pos h']
    have hh := Classical.choose_spec h'
    rw [eq_of_chain hh h]
    simp

Goal state after: