mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ ¬x₀ ∈ Set.range x ∧ Injective x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩

Goal state after:
case refine_1
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ ¬x₀ ∈ Set.range x

case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
let j' := pred j h

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
⊢ insertNthEquiv (fun x ↦ α) (last n) = snocEquiv fun x ↦ α

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ (find? fun x ↦ decide (p x)).get ⋯ = Fin.find p h

Tactic:
by
  simp_rw [find?_decide_eq_dite, Option.get_dite]

Goal state after:
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n.succ - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
succ_eq_add_one,

Goal state after:
r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m * L.prod)
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
IsUnit.mul_iff

Goal state after:
case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
rw [rotate_eq_rotate']
  induction l generalizing l'
  · simp
  · simp_all [rotate']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₂.prod

Tactic:
rw [hl.prod_eq, prod_append]

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j)!

Tactic:
← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _),

Goal state after:
i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j).choose j * j ! * (i + j - j)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m : ℕ
⊢ (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

Tactic:
apply choose_symm_of_eq_add

Goal state after:
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (univ.pi fun a ↦ univ) = univ

Tactic:
ext; simp

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

Goal state before:
pp: case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
· simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
M : Type ?u.6
N : Type ?u.8
inst✝¹ : Semigroup M
inst✝ : Semigroup N
s : Set M
f : M → N
hs : closure s = ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
simp only [← mul_assoc, h₁, h₂]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Tactic:
by rw [← inv_subset_inv, inv_inv]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
⊢ ⇑f ∘ 1 = 1

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_pow hn

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ f a = f 1

Tactic:
map_one

Goal state after:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ f a = 1
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H

pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Tactic:
· rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ f.range = map f ⊤

Tactic:
ext; simp

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : f x = 1
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : f x = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f 1 = 1

Tactic:
map_one

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ y⁻¹ * x ∈ f.ker

Tactic:
by simp [mem_ker, hy']

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ sInf (Subsemigroup.unop ⁻¹' {S | s ⊆ ↑S}) = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set M
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf (Submonoid.unop ⁻¹' {S | s ⊆ ↑S}) = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ f 1 ∈ S

Tactic:
map_one

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
⊢ domRestrict 1 M' = 1

Tactic:
ext; simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝¹ x✝ : M →* A
⊢ (x✝¹ * x✝).domRestrict M' = x✝¹.domRestrict M' * x✝.domRestrict M'

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b : ℕ
h : ¬a < b
ae : (a * a + (a + b)).sqrt = a
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (unpair n).1 < n

Tactic:
simp only [unpair]

Goal state after:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf (Subgroup.unop ⁻¹' {K | s ⊆ ↑K}) = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Tactic:
Set.preimage_ofPred_eq,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
T : Set γ
⊢ (a • b) • T = a • b • T

Tactic:
simp only [← image_smul, image_image, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}

Tactic:
by
  simp_rw [← iUnion_ofPred, ← iUnion_inv_smul, ← preimage_smul, preimage]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (Hx : x ∈ ⨆ i, S i), motive x Hx

Tactic:
refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_

Goal state after:
case refine_1
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : M
hx : x ∈ S i
⊢ ∃ (hm : x ∈ ⨆ i, S i), motive x hm

case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (hm : 1 ∈ ⨆ i, S i), motive 1 hm

case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
by
    rw [Lex.forall, Prod.forall]
    intro a b
    obtain ⟨c, h⟩ := exists_gt b
    use toLex (a, c)
    simpa [lt_iff]

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w

Tactic:
simp only [le_maximum_of_length_pos_iff]
  exact le_maximum_of_mem' h

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
List.max?_eq_some_iff

Goal state after:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a ≤ f b

Tactic:
by rw [← sup_eq_right, ← map_sup, sup_eq_right.2 h]

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

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f b = f a ⊓ f b

Tactic:
inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f b = f b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).min ≠ ↑x

Tactic:
apply mt (congr_arg (WithTop.map toDual))
  rw [map_toDual_min, image_erase toDual.injective, WithTop.map_coe]
  apply max_erase_ne_self

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

pp: case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
· exact bot_le

Goal state after:
case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ f b \ a) = (cons a✝ s✝ h✝).sup f \ a

Tactic:
| cons _ _ _ h =>

Goal state after:
Module: Mathlib.Data.Set.Finite.Powerset

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a}.Finite

Tactic:
by
  convert! ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
  ext s
  simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
    ← and_assoc, Finset.coeEmb] using h.subset

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ ↔ #s < n

Tactic:
refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ → #s < n
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i ↦ a ⊓ f i
⊢ a ⊓ (cons a✝ s✝ h✝).sup f = (cons a✝ s✝ h✝).sup fun i ↦ a ⊓ f i

Tactic:
| cons _ _ _ h =>

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
⊢ α ≃ Fin (card α) → P α

Tactic:
intro e

Goal state after:
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
e : α ≃ Fin (card α)
⊢ P α
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: case zero
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
⊢ PEmpty.{?u.57 + 1} ≃ ULift.{?u.61, 0} (Fin 0) → Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
intro e

Goal state after:
case zero
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty.{?u.57 + 1} = card (ULift.{?u.61, 0} (Fin 0))
e : PEmpty.{?u.57 + 1} ≃ ULift.{?u.61, 0} (Fin 0)
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: case succ
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
⊢ Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
intro e

Goal state after:
case succ
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
e : Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ)
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).inf f

Tactic:
| cons _ _ _ h =>

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (∅.sup f) = ∅.sup fun a ↦ count b (f a)

Tactic:
exact count_zero _

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ (image (fun i ↦ OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
simp only [image_image]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ (image (fun i ↦ OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual ∘ f) s).max' ⋯
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
induction ι using Finite.induction_empty_option with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
by
  rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc
  have := DirectedOn.exists_mem_subset_of_finset_subset_biUnion hn hc hsc
  exact hs.coe_toFinset ▸ this

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b = {a, b}

Tactic:
ext c
  exact h.le_and_le_iff

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s

Tactic:
refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_

Goal state after:
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
⊢ t = s ∨ t = insert x s
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset α
⊢ ↑((map f s).preimage ⇑f ⋯) = ↑s

Tactic:
by simp only [coe_preimage, coe_map, Set.preimage_image_eq _ f.injective]

Goal state after: