mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r n with b | b
  · rcases le_or_gt r (n / 2) with a | h
    · apply choose_le_middle_of_le_half_left a
    · rw [← choose_symm b]
      apply choose_le_middle_of_le_half_left
      lia
  · rw [choose_eq_zero_of_lt b]
    apply zero_le

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype (PLift α)
this : (a : α) → Fintype (PLift (β a))
⊢ Finite ((a : α) → β a)

Tactic:
exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : ConjClasses β
⊢ ∃ a, map f a = b

Tactic:
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Tactic:
simp only [iInter, iInf_subtype']

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
x✝ : 1 ≠ 0
⊢ (s ^ 1).Nontrivial

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ 1 ∈ Set.ofPred IsUnit

Tactic:
by simp only [isUnit_one, Set.mem_ofPred_eq]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ H ≤ K ∨ H ≤ L

Tactic:
or_iff_not_imp_left,

Goal state after:
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ ¬H ≤ K → H ≤ L
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H

Tactic:
simpa

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y

Tactic:
rw [eq_of_mem_singleton hy]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x
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
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f H = f.ker ↔ H = ⊥

Tactic:
comap_eq_ker,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ Disjoint H f.range ↔ H = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp.refine_1.inr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
exact ⟨1, s.one_mem, x, hx, by simp⟩

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
by simp [coe_prod]

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

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]

Goal state after:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: motive : ℕ → Sort u
⊢ Function.Injective fun H n ↦ bitCasesOn n H

Tactic:
intro H₁ H₂ h
  ext b n
  simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable α
f : β → α
finv : α → Option β
linv : ∀ (b : β), finv (f b) = some b
b : β
⊢ (decode (encode (f b))).bind finv = some b

Tactic:
by
    simp [Encodable.encodek, linv]

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

Goal state before:
pp: case h
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)

Tactic:
simpa

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
by simp [coe_prod]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
apply forall_congr'; intro H
  simp only [lt_iff_le_and_ne, le_normalizer, Ne]
  tauto

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
a : α
h : of a = 1
this : (of a).length = length 1
⊢ False

Tactic:
simp only [length_of, length_one, Nat.succ_ne_self] at this

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

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a ∈ z • s⁻¹

Tactic:
simpa

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

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b ∈ z • t⁻¹

Tactic:
simpa

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun x1 x2 ↦ x1 ≤ x2) (map f l) (map g l)

Tactic:
simpa

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x

Tactic:
simpa

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
⊢ Monotone fun i ↦ (take i L).prod

Tactic:
by
  refine monotone_nat_of_le_succ fun n => ?_
  rcases lt_or_ge n L.length with h | h
  · rw [prod_take_succ _ _ h]
    exact le_self_mul
  · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Tactic:
by
  simp only [toLex_le_toLex, lt_iff_le_not_ge, le_antisymm_iff]
  tauto

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
this : ¬p ↑x
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)

Tactic:
simpa

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
rw [closure_singleton_eq, mem_mrange]

Goal state after:
M : Type u_1
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode (n + 1), encode a = n + 1

Tactic:
refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
      rw [encode_some, encode_ofNat]

Goal state after:
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; aesop

Goal state after:
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; aesop

Goal state after:
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 v : Finset (α ⊕ β)
a : α
b : β
ha : inl a ∉ u
⊢ a ∉ u.toLeft

Tactic:
simpa

Goal state after:
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 v : Finset (α ⊕ β)
a : α
b : β
hb : inr b ∉ u
⊢ b ∉ u.toRight

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)

Tactic:
fold,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
    op (Multiset.fold op b₁ (Multiset.map (fun x ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun x ↦ f (inr x)) t.val))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ x < y

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
z : α
hzs : z ∈ s
hz : x < z
⊢ x < z

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id (↑l).toFinset.val).sup

Tactic:
toFinset_val,

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id (↑l).dedup).sup
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
hn : 0 < n
⊢ powersetCard (#s + n) s = ∅

Tactic:
simpa

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

Goal state before:
pp: α : Type u_5
ι : Type u_6
s : Set ι
f : ι → Set α
h : s.PairwiseDisjoint f
x : ↑(⋃ i ∈ s, f i)
⊢ ↑((biUnionEqSigmaOfDisjoint h) x).snd = ↑x

Tactic:
by
  simp [biUnionEqSigmaOfDisjoint]

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

Goal state before:
pp: case inl
ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
h✝ : Subsingleton α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simpa [Subsingleton.elim _ (⊤ : α)]

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
⊢ Injective u

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, ∃ a_2, f a ≤ if a_2 ∈ s then f a_2 else sSup ∅

Tactic:
intro i hi

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ ∃ a, f i ≤ if a ∈ s then f a else sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
· simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Tactic:
have : Nonempty s := Set.Nonempty.to_subtype hs

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : x = b), f x h

Tactic:
by
  refine le_ciSup₂ (f := f) ⟨f b rfl, ?_⟩ b rfl
  rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩
  rfl

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Tactic:
rcases h3.eq_or_lt with (h3 | h3)

Goal state after:
case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ i, f i
⊢ ∃ i, a < f i

Tactic:
by
  contrapose! h
  exact ciSup_le' h

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:
by
  simp_rw [covBy_iff_lt_iff_le_left, iff_comm]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
refine Or.inl (subset_antisymm ?_ hst)
    rwa [← sdiff_singleton_eq_self h, sdiff_singleton_subset_iff]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ a < Function.update a i ci

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
⊢ a i ⩿ b i

Tactic:
refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
  have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j
  refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)
  simp [le_update_iff, h₂.not_ge]

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
⊢ InjOn f ↑(s.preimage f hf)

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case h
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∅.Subsingleton ∧ IsCofinal ∅

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), ¬x ∈ s → ¬P (insert x s)

Tactic:
simp only [not_imp_not]
  exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
h : Set.range ⇑f = Set.range ⇑g
x✝ : α
⊢ Set.range ⇑(OrderEmbedding.ofStrictMono ⇑f ⋯) = Set.range ⇑(OrderEmbedding.ofStrictMono ⇑g ⋯)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
⊢ x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
Set.mem_Icc

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h : ∀ (a b : α), (Set.Icc a b).Finite
a b x : α
⊢ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ range' a b ↔ x ∈ Ico a (a + b)

Tactic:
List.mem_range'_1,

Goal state after:
a b x : ℕ
⊢ a ≤ x ∧ x < a + b ↔ x ∈ Ico a (a + b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a x : ℕ
⊢ x ∈ range' 1 a ↔ x ∈ Icc 1 a

Tactic:
List.mem_range'_1,

Goal state after:
a x : ℕ
⊢ 1 ≤ x ∧ x < 1 + a ↔ x ∈ Icc 1 a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Icc ↑a ↑b) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)

Tactic:
exact refl _

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
rw [Icc_eq_cons_Ico h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)

Tactic:
exact refl _

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (insert a s).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ orbit ⟦a⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq'

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ ↑b ∈ MulAction.orbit ↥H ↑a
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b : Lex (α × β)
hb : b ∈ (fun x ↦ (ofLex x).1) ⁻¹' {a}
c : Lex (α × β)
hc : c ∈ (fun x ↦ (ofLex x).1) ⁻¹' {a}
hbc : b ≤ c
⊢ f b ≤ f c

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hb hc

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
⊢ f b ≤ f c
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
⊢ n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1

Tactic:
simp [← hc _ <| mem_set_normalizer_iff''.mp hn g |>.mp hg]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ ↑C

Tactic:
simpa

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
this : y * z * z⁻¹ ∈ A
⊢ y ∈ ↑A

Tactic:
simpa

Goal state after: