mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count b l ≤ count b l * count b l
h✝² : ¬b = a
h✝¹ : c = b
h✝ : ¬a = b
⊢ count a l + count a l * count b l = count a l * (count b l + 1)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
⊢ s ⊆ image Prod.fst s ×ˢ image Prod.snd s

Tactic:
grind

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

Goal state before:
pp: case inl
n k s : ℕ
hsk : s ≤ k
hnk : n < k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = s.biUnion fun a ↦ image (fun b ↦ (a, b)) t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
b : δ a'
ha' : a' ∈ a' ::ₘ m
⊢ ⋯ ▸ φ b = φ (⋯ ▸ b)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ (s ×ˢ t).biUnion f = s.biUnion fun a ↦ t.biUnion fun b ↦ f (a, b)

Tactic:
grind

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = filter p s ×ˢ filter q t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 = q x.2} = {x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α × α → β
s : Finset α
⊢ image f s.diag = image (fun x ↦ f (x, x)) s

Tactic:
grind

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 : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β 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:
rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag ∪ s.offDiag = s ×ˢ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ (s.pi fun a ↦ {f a}) = {fun a x ↦ f a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.diag = s.offDiag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s ×ˢ s \ s.offDiag = s.diag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (s ∩ t).diag = s.diag ∩ t.diag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (s ∪ t).diag = s.diag ∪ t.diag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.diag = {(a, a)}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
⊢ (insert a s).diag = insert (a, a) s.diag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
has : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
grind

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝¹ : DecidableEq ι
I : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ I
s : Finset ↑I
u : (i : ↑I) → Set (π ↑i)
⊢ I.domRestrict ⁻¹' (↑s).pi u = (↑(image Subtype.val s)).pi fun i ↦ if h : i ∈ I then u ⟨i, h⟩ else Set.univ

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
⊢ u.disjUnion v disj = s.offDiag

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
⊢ ∀ (i : α × α), i ∈ u ↔ (Equiv.prodComm α α) i ∈ v

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i ↦ {f i}) ↔ x✝ ∈ {f}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s t : (a : α) → Finset (δ a)
⊢ (piFinset fun i ↦ s i ∩ t i) = piFinset s ∩ piFinset t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ {f ∈ piFinset t | f a = x} = ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
⊢ piFinset (update s i t) = {f ∈ piFinset s | f i ∈ t}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
a : δ i
ha : a ∈ s i
⊢ piFinset (update s i {a}) = {f ∈ piFinset s | f i = a}

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case zero
a : ℕ
⊢ a.choose 0 ≤ a.succ.choose 0

Tactic:
grind

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

Goal state before:
pp: case succ
a n✝ : ℕ
⊢ a.choose (n✝ + 1) ≤ a.succ.choose (n✝ + 1)

Tactic:
grind

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

Goal state before:
pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
grind

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

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

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [multichoose, IH]; simp [Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty

Tactic:
Set.infinite_image2 hfs hft

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

Tactic:
refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_

Goal state after:
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a✝ : G
ha : a✝ ∈ S
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ b ∈ s, b * a ∈ t
⊢ Function.Injective fun x ↦
    match x with
    | ⟨b, hb⟩ => ⟨b * a, ⋯⟩
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ i, s i)

Tactic:
by
  intro x hx y hy hxy
  rcases mem_iUnion.1 hx with ⟨i, hx⟩
  rcases mem_iUnion.1 hy with ⟨j, hy⟩
  rcases hs i j with ⟨k, hi, hj⟩
  exact hf k (hi hx) (hj hy) hxy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x✝ : β
⊢ x✝ ∈ f '' ⋃₀ s ↔ ∃ i, ∃ (_ : i ∈ s), x✝ ∈ f '' i

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ y ∈ range f, f ⁻¹' {y} = univ

Tactic:
biUnion_preimage_singleton,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ f ⁻¹' range f = univ
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inl
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
x : (i : I) → f i
i : I
⊢ Commute (mulSingle i (x i)) (mulSingle i (x i))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x ↦ Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
⊢ ⇑↑H = Subtype.val

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion ⋯) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑⟨val✝, property✝⟩ ∈ H
⊢ (inclusion h) ⟨↑⟨val✝, property✝⟩, hx⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion hKL) ((inclusion hHK) ⟨val✝, property✝⟩) = (inclusion ⋯) ⟨val✝, property✝⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid G
inv_mem'✝ : ∀ {x : G}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid (Additive G)
neg_mem'✝ : ∀ {x : Additive G}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid A
neg_mem'✝ : ∀ {x : A}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid (Multiplicative A)
inv_mem'✝ : ∀ {x : Multiplicative A}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ↑H = ↑⊤ ↔ ↑H = Set.univ

Tactic:
rfl

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

Goal state before:
pp: N : Type u_5
inst✝ : Group N
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g f.range = (g.comp f).range

Tactic:
rw [range_eq_map, range_eq_map]

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
x✝ : ↥H
⊢ ↑((H.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.subgroupMap H) x✝)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
mem_closure_singleton,

Goal state after:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1, (∃ n, x ^ n = y_1) ∧ ∃ z_1, (∃ n, y ^ n = z_1) ∧ y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: M : Type u_6
inst✝ : CommGroup M
S : Subgroup M
n : ℕ
x✝ : ↥S
⊢ (∃ x ∈ S, x ^ n = ↑x✝) ↔ ∃ a, ∃ (h : a ∈ S), ⟨a ^ n, ⋯⟩ = x✝

Tactic:
grind

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

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toAddSubsemigroup✝ : AddSubsemigroup (Additive M)
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toAddSubsemigroup✝ : AddSubsemigroup A
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toSubsemigroup✝ : Subsemigroup (Multiplicative A)
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ f 1 ∈ S

Tactic:
rw [map_one]; exact S.one_mem

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

Goal state before:
pp: case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ (fst M N) (y1, y2) ∈ s

Tactic:
exact (h hy1).1

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
x✝ : ↥S
⊢ ↑((S.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.submonoidMap S) x✝)

Tactic:
rfl

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑x * ↑y, ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: case inl
x : ℕ
⊢ natSumNatEquivNat (Sum.inl x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inl x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: case inr
x : ℕ
⊢ natSumNatEquivNat (Sum.inr x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inr x)

Tactic:
rfl

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

Goal state before:
pp: case succ.false.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

Tactic:
rfl

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

Goal state before:
pp: case succ.false.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)

Tactic:
rfl

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

Goal state before:
pp: case succ.true.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

Tactic:
rfl

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

Goal state before:
pp: case succ.true.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.div2 < n

Tactic:
grind

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

Goal state before:
pp: case zero
⊢ boddDiv2 0 = (bodd 0, div2 0)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (some x).getD d = x

Tactic:
rfl

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

Goal state before:
pp: case neg.hlt
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₁ < a₂ + b

Tactic:
· exact Nat.lt_add_right _ h

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ none.bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Tactic:
rfl

Goal state after: