mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← reverse_reverse l

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l✝ : List α
n m : ℕ
⊢ l✝.rotate (n + m) = (l✝.rotate n).rotate m

Tactic:
by rw [rotate_rotate]

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)

Tactic:
rw [map_rotate]

Goal state after:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!

Tactic:
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k : ℕ
⊢ multichoose 1 k = 1

Tactic:
induction k with
  | zero => simp
  | succ k IH => simp [multichoose_succ_succ 0 k, IH]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
· simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
    by_contra!
    exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • 1 * y • 1

Tactic:
by rw [smul_one_mul, smul_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
by
  rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
    surjective_iff_surjective_of_iUnion_eq_univ hU]
  simp [Bijective, forall_and]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
p q : Subgroup G
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
q : Subgroup G
hp : Set G
mul_mem'✝ : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem'✝ : 1 ∈ { carrier := hp, mul_mem' := mul_mem'✝ }.carrier
inv_mem'✝ :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ } = q
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'

Tactic:
inf_of_le_right (sup_le hA hA'),

Goal state after:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ A ⊔ A' = B ⊓ A ⊔ B ⊓ A'
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.submonoidMap M') a = ⟨f x, ⋯⟩

Tactic:
exact ⟨⟨x, hx⟩, rfl⟩

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
exact this

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

Goal state before:
pp: case refine_1
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
hx : x ∈ conjugatesOfSet s
⊢ g * x * g⁻¹ ∈ normalClosure s

Tactic:
exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)

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

Goal state before:
pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

Tactic:
rw [← conj_mul]

Goal state after:
case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
rw [insert_eq, mul_union, mul_singleton, mul_singleton]

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
· exact Or.inr (Or.inr <| Lex.right _ _ hba)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
⊢ y ∈ mrange ((powersHom M) x) ↔ ∃ n, x ^ n = y

Tactic:
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.Algebra.Group.Submonoid.Membership

Goal state before:
pp: 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
⊢ IsScalarTower M N α

Tactic:
refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩

Goal state after:
case refine_1
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
⊢ ∀ (y : N) (z : α), (1 • y) • z = 1 • y • z

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
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: 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
⊢ SMulCommClass M N α

Tactic:
refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩

Goal state after:
case refine_1
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
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a

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
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton
α : 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 ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m

Tactic:
foldl_append,

Goal state after:
case append_singleton
α : 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 ∈ foldl (argAux r) (foldl (argAux r) o tl) [a]
⊢ ¬r b m
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a ∈ decode 0, encode a = 0

Tactic:
refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]

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

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

Tactic:
by
  simp [← disjSum_empty, subset_disjSum]

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

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) r₂ (r₁ ++ [l]) = sublists'Aux a r₁ r₂ ++ [a :: l]

Tactic:
foldl_append,

Goal state after:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) (foldl (fun r l ↦ r ++ [a :: l]) r₂ r₁) [l] = sublists'Aux a r₁ r₂ ++ [a :: l]
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl

Tactic:
constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]
    · rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
      · simp
      · simp [ih.mp h]
    · rcases init with - | ⟨hd', tl'⟩
      · simp
      · intro h
        right
        use tl', tail
        simp_all

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ map id (sublistsLen (n + 1) l) ++ (map (id ∘ cons a) (sublistsLen n l) ++ []) =
    sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
map_id,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ (map (id ∘ cons a) (sublistsLen n l) ++ []) =
    sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
have := (pairwise_reverse.2 H).sublists'

Goal state after:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (Lex (Function.swap fun b a ↦ R a b)) l.reverse.sublists'
⊢ Pairwise (Lex R on reverse) l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Tactic:
rw [append_assoc]

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ⊥ \ a

Tactic:
bot_sdiff

Goal state after:
case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ⊥
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset (Finset α)
f : α → β
hf : Set.InjOn f ↑(S.biUnion id)
⊢ ↑S ⊆ ↑(S.biUnion id).powerset

Tactic:
by aesop (add simp Set.subset_def)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
S : Finset β
⊢ S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥

Tactic:
induction S using Finset.induction

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
⊢ ∅.sup f = ⊥ ↔ ∀ s ∈ ∅, f s = ⊥

case insert
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
a✝² : β
s✝ : Finset β
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f = ⊥ ↔ ∀ s ∈ s✝, f s = ⊥
⊢ (insert a✝² s✝).sup f = ⊥ ↔ ∀ s ∈ insert a✝² s✝, f s = ⊥
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (↑(powersetCard n ∅)).Subsingleton

Tactic:
by
  simp [Set.Subsingleton, subset_empty]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ (image f s).sup' hs g = s.sup' ⋯ (g ∘ f)

Tactic:
rw [← WithBot.coe_eq_coe]; simp only [coe_sup', sup_image]; rfl

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

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

Tactic:
count_union,

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a ↦ count b (f a)
⊢ max (count b (f i)) (count b (s.sup f)) = (insert i s).sup fun a ↦ count b (f a)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨆ a ∈ s, g a) = ⨆ a ∈ s, f (g a)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
exact this

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)
⊢ sSup ∅ ≤ max (⨆ x, f x) (sSup ∅)

Tactic:
exact le_sup_right

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)

pp: case neg
α : 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:
case neg
α : 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)
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b

Tactic:
Iio,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ (Finset.Iio b).val ↔ x < b
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x2 < x1
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x2 < x1
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a.swap.toRelHom.toOrderHom n < a.swap.toRelHom.toOrderHom m
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b

Tactic:
by
  rw [← coe_subset, coe_Ico, coe_Icc]
  exact Set.Ico_subset_Icc_self

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ioi ↑a) ↔ a < x

Tactic:
by simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Icc ⊥ ⊤ = univ

Tactic:
rw [Icc_bot, Iic_top]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) [[a, b]] = [[(a, c), (b, c)]]

Tactic:
by
  aesop (add safe forward [le_antisymm])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Icc a b) = Icc (a, c) (b, c)

Tactic:
by
  aesop (add safe forward [le_antisymm])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) [[a, b]] = [[(c, a), (c, b)]]

Tactic:
by
  aesop (add safe forward [le_antisymm])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Icc a b) = Icc (c, a) (c, b)

Tactic:
by
  aesop (add safe forward [le_antisymm])

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 : α
a b : ↑(orbit G x)
⊢ a ∈ orbit (↥H) b ↔ ↑a ∈ orbit ↥H ↑b

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

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : ↑a ∈ orbit ↥H ↑b
⊢ a ∈ orbit (↥H) b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
rw [Iic_sdiff_Ioc, min_eq_left hab]

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
⊢ ↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b

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

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : ↑a ∈ MulAction.orbit ↥H ↑b
⊢ a ∈ MulAction.orbit (↥H) b

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ ∃ k, ∀ (m : ℕ), k < m → f m ∉ s

Tactic:
have := hs.bddAbove_preimage hf

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : BddAbove (f ⁻¹' s)
⊢ ∃ k, ∀ (m : ℕ), k < m → f m ∉ s
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  ¬((∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) ∧
      ∀ (m n : ℕ),
        m < n →
          ¬List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
              (if n < g 0 then f n else (f (g (n - g 0))).tail))
⊢ False

Tactic:
push Not at hf'

Goal state after:
case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
⊢ False
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * (b * g)

Tactic:
← hb g hg,

Goal state after:
M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * (g * b)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t, x ^ f x = ∏ x ∈ t ∪ u, x ^ f x

Tactic:
refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]

Goal state after: