mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup A
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
by cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup (Multiplicative A)
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
by cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H

Tactic:
← top_subgroupOf,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤.subgroupOf K ↔ K ≤ H
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 : x ∈ f.ker
y : G
⊢ f y * f y⁻¹ = 1

Tactic:
map_mul_eq_one f (mul_inv_cancel y)

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 : x ∈ f.ker
y : G
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (⇑(closure s).subtype ⁻¹' s) = ⊤

Tactic:
by
  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 x : Submonoid M
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
by cases x; rfl

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
x : AddSubmonoid (Additive M)
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
by cases x; rfl

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
A : Type u_4
inst✝ : AddZeroClass A
x : AddSubmonoid A
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
by cases x; rfl

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
A : Type u_4
inst✝ : AddZeroClass A
x : Submonoid (Multiplicative A)
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
by cases x; rfl

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
ι : Type u_5
f : F
hf : Surjective ⇑f
S : Submonoid N
x : N
h : x ∈ S
y : M
hy : f y = x
⊢ y ∈ comap f S ∧ f y = x

Tactic:
simp [hy, h]

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: ⊢ ⇑natSumNatEquivNat = Sum.elim (fun x ↦ 2 * x) fun x ↦ 2 * x + 1

Tactic:
ext (x | x)

Goal state after:
case inl
x : ℕ
⊢ natSumNatEquivNat (Sum.inl x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inl x)

case inr
x : ℕ
⊢ natSumNatEquivNat (Sum.inr x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inr x)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + (s + s)

Tactic:
← Nat.add_assoc

Goal state after:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + s + s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Tactic:
refine (image_subset_iff.trans ?_).symm; congr! 1;
  exact ((MulAction.toPerm _).image_eq_preimage_symm _).symm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
    rintro ⟨x, hx⟩
    exact hn.conj_mem _ hx c

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hpl : ∀ (a : α), a ∈ l → p a
⊢ f l.prod ≤ (map f l).prod

Tactic:
induction l with
  | nil => simp [h_one]
  | cons a s ih =>
    have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
    have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
    grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val]

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

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

Tactic:
exact ⟨_, mem _ _ hx⟩

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

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ (FreeMonoid.lift Subtype.val) y ∈ closure s

Tactic:
simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ x ∈ closure s

Tactic:
simp [hs]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ x ∈ closure s

Tactic:
simp [hs]

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

Goal state before:
pp: case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Tactic:
rw [ha]

Goal state after:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ x ∈ s,
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
clear x

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ ∀ x ∈ s,
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
clear x

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

Tactic:
rw [hf] at ho

Goal state after:
case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn none (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'

Tactic:
clear x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'

Tactic:
clear x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ u.toLeft.disjSum u.toRight = u

Tactic:
ext (x | x)

Goal state after:
case inl
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u

case inr
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ map Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft

Tactic:
simp [← disjSum_empty, disjSum_subset]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max = max ↑a ↑b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min = min ↑a ↑b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min' ⋯ = min a b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max' ⋯ = max a b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l'.length = n + 1

Tactic:
by
    rw [sublistsLen_succ_cons, mem_append, mem_map] at h
    rcases h with (h | ⟨l', h, rfl⟩)
    · exact length_of_sublistsLen h
    · exact congr_arg (· + 1) (length_of_sublistsLen h)

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++ flatMap (fun n ↦ sublistsLen n (h :: tl)) (map succ (range (tl.length + 1))) ~
    (h :: tl).sublists'

Tactic:
flatMap_map,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++ flatMap (fun a ↦ sublistsLen a.succ (h :: tl)) (range (tl.length + 1)) ~
    (h :: tl).sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

Tactic:
refine
    (biUnion_sdiff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_sdiff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)
  rw [mem_iUnion₂]; rintro ⟨j, hj, haj⟩
  exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ⊆ (powersetCard n.succ u).sup id

Tactic:
rw [sup_eq_biUnion, subset_iff]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id
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)))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]

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))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r.succ ≠ 0
hrs : r.succ ≤ #s
⊢ (powersetCard r.succ s).sup id = s

Tactic:
exact powersetCard_sup _ _ hrs

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

Goal state before:
pp: case insert.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s = ∅
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)

Tactic:
simp [hs]

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

Goal state before:
pp: case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
rw [he i hi, mem_empty_iff_false] at hx

Goal state after:
case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : False
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (⋃ y ∈ s, f ⁻¹' {y}).Finite

Tactic:
exact Set.Finite.biUnion h hf

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Tactic:
constructor
  · intro h x hx
    refine h.trans_le (csInf_le ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]
  · intro H
    have := hs.ciInf_mem_image _ h
    simp only [mem_image] at this
    obtain ⟨_, hmem, hx⟩ := this
    rw [← hx]
    exact H _ hmem

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
rw [ciSup_of_not_bddAbove hg, ciSup_of_not_bddAbove <| mt bbdAbove_range_right_of_sup hg]
    exact le_sup_right

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
o : Option α
f : α → β
⊢ ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
simp [iSup, h, le_csSup_iff', upperBounds]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a

Tactic:
wcovBy_iff_covBy_or_le_and_le

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⋖ b ∨ a ≤ b ∧ b ≤ a ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅

Tactic:
by
      simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y

Tactic:
covBy_iff_lt_iff_le_left,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ (∀ {z : α}, z < y ↔ z ≤ x) ↔ ∀ {z : α}, z ≤ x ↔ z < y
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
wcovBy_iff_covBy_or_le_and_le

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ a ⩿ b → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b

Tactic:
· intro h
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
    exact ⟨i, h.eval _, hi⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (x ∈ if h : True then map (Embedding.sigmaMk i) (f a b) else ∅) →
    ∃ (h : i = x.fst) (h_1 : i = x.fst), x.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)

Tactic:
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]

Goal state after:
case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ ∀ x_1 ∈ f a b, ⟨i, x_1⟩ = x → ∃ (h : i = x.fst) (h_1 : i = x.fst), x.snd ∈ f (⋯ ▸ a) (⋯ ▸ b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ max a b + 1 - min a b = (↑b - ↑a).natAbs + 1

Tactic:
by rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

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

Goal state before:
pp: P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | ∀ m ≥ x, P m}
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

pp: P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hb : n + b + 1 ≤ b
hn : ∀ m > n, P m
⊢ False

Tactic:
all_goals lia

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
⊢ WellQuasiOrdered s

Tactic:
by
  intro seq
  have ⟨_, _, hle, hr⟩ := h (Function.surjInv hf ∘ seq)
  exact ⟨_, _, hle, by simpa [Function.surjInv_eq] using f.map_rel hr⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n

Tactic:
cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl

Goal state after: