mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a

Tactic:
| _ s
   => 

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
by
  rw [sup_eq_closure_mul]
  refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
  induction hx using closure_induction'' with
  | one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
  | mem _ hx => exact hx
  | inv_mem x hx =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
  | mul x' x' _ _ hx hx' =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    obtain ⟨x', hx', y', hy', rfl⟩ := hx'
    refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
    · simp only [mul_assoc, mul_inv_cancel_left]

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

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝

Tactic:
· rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩
    refine ⟨?_, mul_mem (h hy) hzC⟩
    exact ⟨y, hy, z, hzB, rfl⟩

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ s₁.noncommProd f comm = s₂.noncommProd g ⋯

Tactic:
by
  simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using!
    Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b = (b * a⁻¹ ∈ s)

Tactic:
by
    simp only [eq_iff_iff]
    apply rightRel_apply

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ * ↑⟨1, hs⟩ = x✝ * ↑⟨1, hs⟩
⊢ ↑⟨1, hs⟩ * x✝¹ = ↑⟨1, hs⟩ * x✝

Tactic:
rw [mul_one, mul_one] at h

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ = x✝
⊢ ↑⟨1, hs⟩ * x✝¹ = ↑⟨1, hs⟩ * x✝
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x + y) = x + y

Tactic:
FreeAbelianGroup.map_add,

Goal state after:
α : Type u
G : Type u_1
β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> x + id <$> y = x + y
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> (y₁ + y₂) = (fun b a ↦ (a, b)) <$> (y₁ + y₂) <*> pure p

Tactic:
FreeAbelianGroup.map_add,

Goal state after:
case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> (y₁ + y₂) <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> (y₁ + y₂) <*> pure p

Tactic:
FreeAbelianGroup.map_add,

Goal state after:
case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₁ + (fun b a ↦ (a, b)) <$> y₂ <*> pure p
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one] at h1 h2 ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅g₁, g₂⁆⁆ = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ Prod.mk <$> (x₁ + x₂) <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁ + x₂

Tactic:
FreeAbelianGroup.map_add,

Goal state after:
case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ Prod.mk <$> x₁ + Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁ + x₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : CommMonoid M
a : M
s : Multiset M
ih : IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a
⊢ IsUnit (a ::ₘ s).prod ↔ ∀ a_1 ∈ a ::ₘ s, IsUnit a_1

Tactic:
| cons a s ih =>

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P r₁ s₁ = P r₂ s₂

Tactic:
hP r₁ v s₁ s₁vS,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (v • r₁) ⟨v * ↑s₁, s₁vS⟩ = P r₂ s₂
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g (f.sec z).1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * g ↑(f.sec z).2) = g (f.sec z).1

Tactic:
← g.domRestrict_apply,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g (f.sec z).1 * (↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ * (g.domRestrict S) (f.sec z).2) =
    g (f.sec z).1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.coe.top
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
this✝ : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
x : R
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
this : ↑(f x) ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
simp [mul_top hx, mul_top this]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
⊢ ↑a * b * c = ↑a * (b * c)

Tactic:
| coe a =>

Goal state after:
case inr.inr.inr.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
⊢ ↑a * b * c = ↑a * (b * c)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n

Tactic:
cases n with

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
rintro ⟨m, hm⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
⊢ False
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
⊢ ∃ x, IsGreatest S x

Tactic:
obtain ⟨m, hm⟩ := hS

Goal state after:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS' : S.Nonempty
m : X
hm : m ∈ upperBounds S
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ succ x

Tactic:
exact covBy_succ x

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a = succ ⊥ ∨ a = ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Tactic:
or_comm

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a = ⊥ ∨ a = succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
⊢ False

Tactic:
| coe a =>

Goal state after:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat

Tactic:
· rename_i a; cases a <;> simp

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ {i}.piecewise f g = update g i (f i)

Tactic:
← insert_empty_eq,

Goal state after:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ (insert i ∅).piecewise f g = update g i (f i)
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
u : Finset (α ⊕ β)
⊢ u.toRight = univ ↔ map Function.Embedding.inr univ ⊆ u

Tactic:
simp [map_inr_subset_iff_subset_toRight]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a ∈ univ, b ↑a = i

Tactic:
subst ha

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ (image b univ).erase k
⊢ ∃ a_1 ∈ univ, b ↑a_1 = b a
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i

Tactic:
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a b : α
f : α → β
m : Multiset α
hc : m.card = n
⊢ (Multiset.map f m).card = n

Tactic:
by simp [hc]

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩ w

Tactic:
rcases w with ⟨_ | ⟨b, w⟩, w_property⟩

Goal state after:
case succ.cons.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : (a :: v).length = n + 1
w_property : [].length = n + 1
⊢ C ⟨a :: v, v_property⟩ ⟨[], w_property⟩

case succ.cons.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : (a :: v).length = n + 1
b : β
w : List β
w_property : (b :: w).length = n + 1
⊢ C ⟨a :: v, v_property⟩ ⟨b :: w, w_property⟩
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False

Tactic:
exact hb.2 hb.1.2.symm

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : v.length = n
⊢ F (Vector β v.length) = F (Vector β n)

Tactic:
Hv

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : v.length = n
⊢ F (Vector β n) = F (Vector β n)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
· exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by
  simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝¹, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝¹ ≤ ↑a✝

Tactic:
simp only [lex_inl_inl, coe_le_coe]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ IsLUB (g ∘ f '' d) ((g ∘ f) a)

Tactic:
have hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d) := by
    have := hf.monotone
    simp only [Monotone, DirectedOn, mem_image, exists_exists_and_eq_and, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂] at ⊢ this hd₃
    grind

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
⊢ IsLUB (g ∘ f '' d) ((g ∘ f) a)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ f (ωSup₀ c)

Tactic:
rw [h']

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ f (c i) ≤ ωSup (c.map f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ f (ωSup₀ c) ≤ f x

Tactic:
rw [h']

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ ωSup (c.map f) ≤ f x
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set α
hc₁ : ChainClosure r s✝
h : s✝ ⊆ c₂
⊢ SuccChain r s✝ ⊆ c₂

Tactic:
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
⊢ a = b

Tactic:
have := c.monotone hji _ hb

Goal state after:
case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i, f i)

Tactic:
rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:

Tactic:
#α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

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

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
f g : A →ₑ*[φ] B
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨tF, _, _⟩

Goal state after:
M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
g : A →ₑ*[φ] B
tF : A →ₑ[⇑φ] B
map_one'✝ : tF.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
h : (fun m ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun m ↦ m.toFun) g
⊢ { toMulActionHom := tF, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g