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

Goal state before:
pp: n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩

Goal state after:
n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
⊢ n ≤ m
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_of_lt]

Goal state after:
case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i + 1)) % n = (m * n - (↑i / n * n + ↑i % n + 1)) % n

Tactic:
by rw [Nat.div_add_mod']

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i

Tactic:
rw [Fin.not_le] at hi

Goal state after:
case neg
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (i.pred ⋯) = i

Tactic:
succAbove_pred_of_lt _ _ h

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
· rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (i.pred ⋯) = i

Tactic:
succAbove_pred_of_lt _ _ h

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove i.castSucc = i

Tactic:
predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h

Goal state after:
case inr
n : ℕ
p i : Fin n
h : i < p
⊢ i = i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ Set.range Subtype.val

Tactic:
rwa [Subtype.range_coe_subtype]

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
x : Fin (m + n)
⊢ Sum.elim (castAdd n) (natAdd m) ((fun i ↦ addCases Sum.inl Sum.inr i) x) = x

Tactic:
by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp

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

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)

Tactic:
· simp [rev_succAbove]

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
by
  classical
    rw [duplicate_iff_two_le_count, ← replicate_sublist_iff,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
    constructor
    · rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp
    · rintro ⟨n, m, hnm, h, h'⟩
      refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite

Tactic:
by simpa using hs.union h

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite

Tactic:
by simpa using hs.union h

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (range n.succ))

Tactic:
range_succ_eq_map

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : ¬a ∈ s
⊢ count a s ≤ count a (s.card • t)

pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ count a s ≤ count a (s.card • t)

Tactic:
· simp [count_eq_zero_of_notMem has]

Goal state after:
case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ count a s ≤ count a (s.card • t)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ count a (s.card • t)

Tactic:
count_nsmul,

Goal state after:
case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ s.card * count a t
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Tactic:
rw [← reverse_reverse l]
  simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
    length_reverse]
  rw [← length_reverse]
  let k := n % l.reverse.length
  rcases hk' : k with - | k'
  · simp_all! [k, length_reverse, ← rotate_rotate]
  · rcases l with - | ⟨x, l⟩
    · simp
    · rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
this : map (fun x ↦ (x.fst, a)) l.zipIdx = map (fun x ↦ (x, a)) l
⊢ flatMap (fun x ↦ map (Prod.mk x.fst) ((a :: l).eraseIdx x.snd)) ((a, 0) :: map (Prod.map id fun x ↦ x + 1) l.zipIdx) ~
    map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++
      flatMap (fun x ↦ map (Prod.mk x.fst) (l.eraseIdx x.snd)) l.zipIdx

Tactic:
simp [append_assoc, perm_append_left_iff, flatMap_map,
    ← (map_append_flatMap_perm _ _ _).congr_left, this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
⊢ Finite (α × β)

Tactic:
have := H.1 ⟨b⟩

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this : Finite α
⊢ Finite (α × β)
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ FactorsThrough f s.domRestrict

Tactic:
rw [DependsOn, FactorsThrough]
  simp [funext_iff]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
· subst eq; rfl

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case of_succ
n r k : ℕ
hk : k < n / 2
ih : n.choose (k + 1) ≤ n.choose (n / 2)
⊢ n.choose k ≤ n.choose (n / 2)

Tactic:
exact (choose_le_succ_of_lt_half_left hk).trans ih

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

Goal state before:
pp: case closure
M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Subsemigroup.closure s = ⊤

Tactic:
exact closure

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a}⁻¹ = {a⁻¹}

Tactic:
rw [← image_inv_eq_inv, image_singleton]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a}⁻¹ = {b}

Tactic:
rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]

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

Goal state before:
pp: case closure
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ Submonoid.closure s = ⊤

Tactic:
exact closure

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : f x = f y
⊢ x = y

Tactic:
rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy

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
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
by
  constructor
  · intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (inl M N) x1 ∈ u

Tactic:
apply hH

Goal state after:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (inl M N) x1 ∈ map (inl M N) s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Normal ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H

Tactic:
← normalizer_eq_top_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalizer ↑H = ⊤ ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsIdempotentElem a
n : ℕ
hn : n ≠ 0
⊢ a ^ n = a

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsIdempotentElem a
i : ℕ
hn : i + 1 ≠ 0
⊢ a ^ (i + 1) = a
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H

Tactic:
apply iInf_le_of_le 1

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ map (↑(MulAut.conj 1)) H ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ (Subgroup.map f H).Normal

Tactic:
← normalizer_eq_top_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ normalizer ↑(Subgroup.map f H) = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]

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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
refine ⟨z, ?_⟩

Goal state after:
case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Module: Mathlib.Algebra.Group.Subgroup.Basic

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).Normal ↔ H.Normal

Tactic:
← normalizer_eq_top_iff,

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
⊢ normalizer ↑(comap f H) = ⊤ ↔ H.Normal
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ x, S ↑x ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
mem_iSup_of_directed

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

case hS
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ

pp: M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = ?m.52

Tactic:
· exact (length l)

Goal state after:
M : Type u_3
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedMonoid M
inst✝ : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.length = l.length
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
exact left _ _ ha

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

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
by rw [← decode_eq_ofNat, decode_sigma_val]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a

Tactic:
rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

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

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

Tactic:
by
  apply maximum_mem
  simp only [coe_maximum_of_length_pos]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
⊢ (s.sup fun x ↦ ⊥) = ⊥

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
  · exact sup_empty
  · exact sup_const hs _

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

Goal state before:
pp: case inl.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' ↦ ⨆ i ∈ s, f (i, i')) (i, j').2

Tactic:
convert! le_iSup₂ (α := α) i hj.1; rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ ⨆ x, a = a

Tactic:
iSup,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ sSup (range fun x ↦ a) = a
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
iSup,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (sSup (range fun i ↦ f i)) = ⨆ i, l (f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
iSup,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ sSup (Set.range fun i ↦ ⨆ (_ : i ∈ s), f i) = (image f s).max' h'
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
iSup,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(sSup (range fun i ↦ f i)) = ⨆ i, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(sSup (range fun i ↦ f i)) = ⨆ i, ↑(f i)

Tactic:
iSup,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ ↑(sSup (range fun i ↦ f i)) = sSup (range fun i ↦ ↑(f i))
Module: Mathlib.Data.Set.Finite.Lattice

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

Tactic:
suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    have : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  have := hs.to_subtype
  have : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove (range fun i ↦ f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (f '' s) = ⨆ i, f ↑i

Tactic:
iSup,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove (range fun i ↦ f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (f '' s) = sSup (range fun i ↦ f ↑i)
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)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
· rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]
    exact le_sup_left

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)