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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.closure (⇑f '' {x}) = Subgroup.closure {f x}

Tactic:
Set.image_singleton

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.closure {f x} = Subgroup.closure {f x}
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) none) =
    none.bind fun a ↦ Option.map (Prod.mk a) none

Tactic:
rfl

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

Goal state before:
pp: case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) none

Tactic:
rfl

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

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝¹).bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩

Tactic:
rfl

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

Goal state before:
pp: M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi s = I.pi (c • s)

Tactic:
lift c to Mˣ using hc
  exact smul_set_pi c I s

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b ↦ op b • a) t s = image2 (fun x1 x2 ↦ x1 * x2) t s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b

Tactic:
rfl

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

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

Tactic:
conv_rhs => rw [← Equiv.iInf_comp (Equiv.mulLeft g)]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ map (↑(MulAut.conj g)) (⨅ g, map (↑(MulAut.conj g)) H) = ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
a : α
⊢ of a ≠ 1

Tactic:
by
  intro h
  have := congrArg FreeMonoid.length h
  simp only [length_of, length_one, Nat.succ_ne_self] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f : α → M
x✝¹ x✝ : FreeMonoid α
⊢ prodAux (List.map f (toList (x✝¹ * x✝))) = prodAux (List.map f (toList x✝¹)) * prodAux (List.map f (toList x✝))

Tactic:
by simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ (map f) 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ (map f) (of a * b) = of (f a) * (map f) b

Tactic:
rfl

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
s : Set N
f : G ≃* N
⊢ normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

Tactic:
by
  have := f.toEquiv.image_symm_eq_preimage s
  simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]

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

Goal state before:
pp: case nil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
⊢ [].prod ≤ [].prod

Tactic:
rfl

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

Goal state before:
pp: case slnil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ [].prod ≤ [].prod

Tactic:
rfl

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

Goal state before:
pp: case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ [].prod

Tactic:
rfl

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

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ ∀ (x : M), x ∈ b :: l → 1 < x

Tactic:
grind

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

Goal state before:
pp: ι : 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.Total (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Goal state after:
case inl
ι : 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.Total (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

case inr.inl
ι : 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.Total (s i)
i : ι
a b : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

case 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.Total (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : 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 : α i
j : ι
b : α j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Goal state after:
case inl
ι : 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 : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

case inr.inl
ι : 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
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

case 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 : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ < a₂ ∨ a₁ = a₂ ∧ b₁ < b₂) ∧ ∀ (a : α) (b : β), a₁ < a ∨ a₁ = a ∧ b₁ < b → ¬(a < a₂ ∨ a = a₂ ∧ b < b₂)) ↔
    (a₁ = a₂ ∧ b₁ < b₂ ∧ ∀ ⦃c : β⦄, b₁ < c → ¬c < b₂) ∨
      (a₁ < a₂ ∧ ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂) ∧ (∀ (b : β), ¬b₁ < b) ∧ ∀ (b : β), ¬b < b₂

Tactic:
grind

Goal state after:
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
⊢ l.length = l.length

Tactic:
rfl

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 // p x ∨ q x }
⊢ Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯))
      ((subtypeOrLeftEmbedding p q) x) =
    x

Tactic:
grind

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

Goal state before:
pp: case inl
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯))
        (Sum.inl x)) =
    Sum.inl x

Tactic:
grind

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

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ Sum.inr ⟨↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x), ⋯⟩ = Sum.inr x

Tactic:
grind

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
x : α
hx : x ∈ s i
hx' : (fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s i
⊢ ⟨i, ⟨x, hx⟩⟩ = ⟨i, ⟨(fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a n✝ n : M
i : ℕ
⊢ n✝ ^ i = n ↔ ((powersHom M) n✝) i = n

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) (some val✝) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp only
      split_ifs <;> simp

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

Goal state before:
pp: case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = none
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) none → m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
grind

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

Goal state before:
pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ val✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = some val✝
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (some val✝) → m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
grind

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y

Tactic:
rfl

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

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
mem_closure_singleton,

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y, (∃ n, a ^ n = y) ∧ ∃ z, (∃ n, b ^ n = z) ∧ y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map (f ∘ inl) s + map (f ∘ inr) t = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
Function.comp_def

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (List.range ↑x)).length = #({y ∈ range ↑x | y ∈ s})

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l

Tactic:
intro _ h a hal hma

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ idxOf m l ≤ idxOf a l
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({y ∈ range ↑(succ (ofNat s n)) | y ∈ s}) = n + 1

Tactic:
rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({x ∈ range ↑(succ (ofNat s n)) | x ∈ s})
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← TopHom.comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g a) ⊔ f (g b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap [] = [].zip l₁

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
simp only [min', inf'_image]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
simp only [min', inf'_image]
  exact .symm <| apply_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ ¬(image (⇑toDual) (s.erase x)).max = WithTop.map ⇑toDual ↑x

Tactic:
image_erase toDual.injective,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ ¬((image (⇑toDual) s).erase (toDual x)).max = WithTop.map ⇑toDual ↑x
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).min ≠ ↑x

Tactic:
by
  apply mt (congr_arg (WithTop.map toDual))
  rw [map_toDual_min, image_erase toDual.injective, WithTop.map_coe]
  apply max_erase_ne_self

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (do
      let x ← [a].sublists
      map (fun x_1 ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
sublists_singleton,

Goal state after:
α : Type u
l : List α
a : α
⊢ (do
      let x ← [[], [a]]
      map (fun x_1 ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
⊢ [].reverse.sublists = map reverse [].sublists'

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
hd : α
tl : List α
ih : tl.reverse.sublists = map reverse tl.sublists'
⊢ (hd :: tl).reverse.sublists = map reverse (hd :: tl).sublists'

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ [] ++ [a] = pure a

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) ∘ cons a = g ∘ f ∘ cons a

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : List α → β
r : List β
head✝ : α
tail✝ : List α
⊢ sublistsLenAux 0 (head✝ :: tail✝) f r = f [] :: r

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) [[]] = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]

Tactic:
rfl

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

Goal state before:
pp: case succ.slnil
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (n + 1) [] <+ sublistsLen (n + 1) []

Tactic:
rfl

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

Goal state before:
pp: case succ.nil
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
⊢ powersetCardAux (n + 1) [] ~ powersetCardAux (n + 1) []

Tactic:
rfl

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

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ∅.sup (f ⊔ g) = ∅.sup f ⊔ ∅.sup g

Tactic:
rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : (⋃ a ∈ s, a).Pairwise r
a : Set α
ha : a ∈ s
⊢ a ⊆ a

Tactic:
rfl

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

Goal state before:
pp: case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝

Tactic:
rfl

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

Goal state before:
pp: case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥

Tactic:
rfl

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 = (↑l).dedup.sup

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
x✝⁴ : Finset α
x✝³ : x✝⁴ ∈ ↑s.powerset
x✝² : Finset α
x✝¹ : x✝² ∈ ↑s.powerset
x✝ : (fun x ↦ image f x) x✝⁴ = (fun x ↦ image f x) x✝²
⊢ x✝⁴ = x✝²

Tactic:
grind

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

Goal state before:
pp: case e'_3
α : 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, i') = f (i, (i, i').2)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
t : Finset β
ht : t ∈ ↑(image f s).powerset
⊢ {x ∈ s | f x ∈ t} ∈ ↑s.powerset ∧ (fun x ↦ image f x) ({x ∈ s | f x ∈ t}) = t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : Finset β
x✝ : a ∈ (image f s).powerset
⊢ {x ∈ s | f x ∈ a} ∈ s.powerset ∧ image f ({x ∈ s | f x ∈ a}) = a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : Finset β
⊢ a ∈ image (fun x ↦ image f x) s.powerset → a ∈ (image f s).powerset

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
t : Finset α
⊢ t.erase a ⊆ s ↔ t ⊆ s ∨ ∃ a_1 ⊆ s, insert a a_1 = t

Tactic:
grind

Goal state after: