mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case pos
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : p a
⊢ {a}.bind f = f a

pp: case neg
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : ¬p a
⊢ bind 0 f = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : p a
⊢ {a}.bind f = f a

case neg
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
ham : a ∈ m
h✝ : ¬p a
⊢ bind 0 f = 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'

Tactic:
<;>

Goal state after:
case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
hf : (↑∅).PairwiseDisjoint f
⊢ Disjoint (∅.disjiUnion f hf) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

pp: case cons
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (hf : (↑s✝).PairwiseDisjoint f), Disjoint (s✝.disjiUnion f hf) t ↔ ∀ i ∈ s✝, Disjoint (f i) t
hf : (↑(cons a✝¹ s✝ h✝)).PairwiseDisjoint f
⊢ Disjoint ((cons a✝¹ s✝ h✝).disjiUnion f hf) t ↔ ∀ i ∈ cons a✝¹ s✝ h✝, Disjoint (f i) t

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
hf : (↑∅).PairwiseDisjoint f
⊢ Disjoint (∅.disjiUnion f hf) t ↔ ∀ i ∈ ∅, Disjoint (f i) t

case cons
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : ∀ (hf : (↑s✝).PairwiseDisjoint f), Disjoint (s✝.disjiUnion f hf) t ↔ ∀ i ∈ s✝, Disjoint (f i) t
hf : (↑(cons a✝¹ s✝ h✝)).PairwiseDisjoint f
⊢ Disjoint ((cons a✝¹ s✝ h✝).disjiUnion f hf) t ↔ ∀ i ∈ cons a✝¹ s✝ h✝, Disjoint (f i) t
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℕ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

pp: case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n

Tactic:
<;>

Goal state after:
case empty
n : ℕ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℕ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

pp: case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n

Tactic:
<;>

Goal state after:
case empty
n : ℕ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℤ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

pp: case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n

Tactic:
<;>

Goal state after:
case empty
n : ℤ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℤ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

pp: case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n

Tactic:
<;>

Goal state after:
case empty
n : ℤ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
by
  simp only [Finset.Nonempty, mem_biUnion]
  rw [exists_comm]
  simp [exists_and_left]

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

Goal state before:
pp: case empty
α : Type u_1
β : Type v
t : Multiset β
⊢ map Prod.swap (0 ×ˢ t) = t ×ˢ 0

pp: case cons
α : Type u_1
β : Type v
t : Multiset β
a✝¹ : α
s✝ : Multiset α
a✝ : map Prod.swap (s✝ ×ˢ t) = t ×ˢ s✝
⊢ map Prod.swap ((a✝¹ ::ₘ s✝) ×ˢ t) = t ×ˢ (a✝¹ ::ₘ s✝)

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
β : Type v
t : Multiset β
⊢ map Prod.swap (0 ×ˢ t) = t ×ˢ 0

case cons
α : Type u_1
β : Type v
t : Multiset β
a✝¹ : α
s✝ : Multiset α
a✝ : map Prod.swap (s✝ ×ˢ t) = t ×ˢ s✝
⊢ map Prod.swap ((a✝¹ ::ₘ s✝) ×ˢ t) = t ×ˢ (a✝¹ ::ₘ s✝)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
⊢ (map f (0 ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) 0).prod

pp: case cons
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
a✝¹ : α
s✝ : Multiset α
a✝ : (map f (s✝ ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s✝).prod
⊢ (map f ((a✝¹ ::ₘ s✝) ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) (a✝¹ ::ₘ s✝)).prod

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
⊢ (map f (0 ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) 0).prod

case cons
α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
t : Multiset β
f : α × β → M
a✝¹ : α
s✝ : Multiset α
a✝ : (map f (s✝ ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s✝).prod
⊢ (map f ((a✝¹ ::ₘ s✝) ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) (a✝¹ ::ₘ s✝)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

pp: case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []

Tactic:
<;>

Goal state after:
case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
k n : ℕ
this : ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length
hn : n < ([].rotate k).cyclicPermutations.length
hn' : n < ([].cyclicPermutations.rotate k).length
⊢ [].rotate ((↑⟨n, hn⟩ + k) % [].length) = [].cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % [].cyclicPermutations.length, ⋯⟩

pp: case cons
α : Type u
k n : ℕ
head✝ : α
tail✝ : List α
this : ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
hn : n < ((head✝ :: tail✝).rotate k).cyclicPermutations.length
hn' : n < ((head✝ :: tail✝).cyclicPermutations.rotate k).length
⊢ (head✝ :: tail✝).rotate ((↑⟨n, hn⟩ + k) % (head✝ :: tail✝).length) =
    (head✝ :: tail✝).cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % (head✝ :: tail✝).cyclicPermutations.length, ⋯⟩

Tactic:
<;>

Goal state after:
case nil
α : Type u
k n : ℕ
this : ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length
hn : n < ([].rotate k).cyclicPermutations.length
hn' : n < ([].cyclicPermutations.rotate k).length
⊢ [].rotate ((↑⟨n, hn⟩ + k) % [].length) = [].cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % [].cyclicPermutations.length, ⋯⟩

case cons
α : Type u
k n : ℕ
head✝ : α
tail✝ : List α
this : ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
hn : n < ((head✝ :: tail✝).rotate k).cyclicPermutations.length
hn' : n < ((head✝ :: tail✝).cyclicPermutations.rotate k).length
⊢ (head✝ :: tail✝).rotate ((↑⟨n, hn⟩ + k) % (head✝ :: tail✝).length) =
    (head✝ :: tail✝).cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % (head✝ :: tail✝).cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 0 = 1

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).choose 0 = 1

Tactic:
<;>

Goal state after:
case zero
⊢ choose 0 0 = 1

case succ
n✝ : ℕ
⊢ (n✝ + 1).choose 0 = 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 0 = 1

pp: case succ
n✝ : ℕ
a✝ : n✝.choose n✝ = 1
⊢ (n✝ + 1).choose (n✝ + 1) = 1

Tactic:
<;>

Goal state after:
case zero
⊢ choose 0 0 = 1

case succ
n✝ : ℕ
a✝ : n✝.choose n✝ = 1
⊢ (n✝ + 1).choose (n✝ + 1) = 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 1 = 0

pp: case succ
n✝ : ℕ
a✝ : n✝.choose 1 = n✝
⊢ (n✝ + 1).choose 1 = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
⊢ choose 0 1 = 0

case succ
n✝ : ℕ
a✝ : n✝.choose 1 = n✝
⊢ (n✝ + 1).choose 1 = n✝ + 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ 0 * (0 + 1) / 2 = 0 * (0 - 1 + 2) / 2

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1) * (n✝ + 1 + 1) / 2 = (n✝ + 1) * (n✝ + 1 - 1 + 2) / 2

Tactic:
<;>

Goal state after:
case zero
⊢ 0 * (0 + 1) / 2 = 0 * (0 - 1 + 2) / 2

case succ
n✝ : ℕ
⊢ (n✝ + 1) * (n✝ + 1 + 1) / 2 = (n✝ + 1) * (n✝ + 1 - 1 + 2) / 2
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (b, b) l.offDiag = count b l * count b 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✝¹ : c = b
h✝ : a = b
⊢ count b l + count b l + (count b l * count b l - count b l) = (count b l + 1) * (count b l + 1) - (count b l + 1)

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 a l ≤ count a l * count a l
h✝¹ : c = a
h✝ : ¬a = b
⊢ count b l + count a l * count b l = (count a l + 1) * count b l

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:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (b, b) l.offDiag = count b l * count b 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✝¹ : c = b
h✝ : a = b
⊢ count b l + count b l + (count b l * count b l - count b l) = (count b l + 1) * (count b l + 1) - (count b l + 1)

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 a l ≤ count a l * count a l
h✝¹ : c = a
h✝ : ¬a = b
⊢ count b l + count a l * count b l = (count a l + 1) * count b l

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, i ≠ j ∧ l[i] = x ∧ l[j] = y) ↔ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ x ≠ y

Tactic:
Ne

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) ↔ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n a b : ℕ
h : n = a + b
⊢ n.choose a = n.choose b

Tactic:
suffices choose n (n - b) = choose n b by
    rw [h, Nat.add_sub_cancel_right] at this; rwa [h]
  exact choose_symm (h ▸ le_add_left _ _)

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

Goal state before:
pp: m : ℕ
⊢ 2 * m + 1 = m + 1 + m

Tactic:
rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a ↦ ↑(t a)

Tactic:
by
    rw [Set.mem_univ_pi]
    exact Fintype.mem_piFinset

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

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

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

Tactic:
<;>

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

case succ
a n✝ : ℕ
⊢ a.choose (n✝ + 1) ≤ a.succ.choose (n✝ + 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ multichoose 0 0 = 1

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).multichoose 0 = 1

Tactic:
<;>

Goal state after:
case zero
⊢ multichoose 0 0 = 1

case succ
n✝ : ℕ
⊢ (n✝ + 1).multichoose 0 = 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
multichoose_succ_succ,

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ n.multichoose (k + 1) + (n + 1).multichoose k = (n + 1 + (k + 1) - 1).choose (k + 1)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
hy : y ∈ ⋂ i, f '' s i
⊢ y ∈ f '' ⋂ i, s i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case pos
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

pp: case neg
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : ¬i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

Tactic:
<;>

Goal state after:
case pos
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k

case neg
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
h✝ : ¬i = k
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
have hk := congr_fun h k
    have hl := congr_fun h l
    have hm := congr_fun h m
    have hn := congr_fun h n
    grind [mul_one, one_mul, mul_apply]

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

Goal state before:
pp: case rs
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

pp: case rt
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n

Tactic:
<;>

Goal state after:
case rs
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

case rt
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s

pp: case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t

Tactic:
<;>

Goal state after:
case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s

case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}

pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}

Tactic:
<;>

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}

case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.ofNat a✝ ≠ 0
⊢ ∅ ^ Int.ofNat a✝ = ∅

pp: case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.negSucc a✝ ≠ 0
⊢ ∅ ^ Int.negSucc a✝ = ∅

Tactic:
<;>

Goal state after:
case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.ofNat a✝ ≠ 0
⊢ ∅ ^ Int.ofNat a✝ = ∅

case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a✝ : ℕ
hn : Int.negSucc a✝ ≠ 0
⊢ ∅ ^ Int.negSucc a✝ = ∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

pp: case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}

Tactic:
<;>

Goal state after:
case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ a⁻¹ * x) fun x ↦ a * x
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a⁻¹ * x) ((fun x ↦ a * x) c) = c

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a * x) ((fun x ↦ a⁻¹ * x) c) = c

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a⁻¹ * x) ((fun x ↦ a * x) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a * x) ((fun x ↦ a⁻¹ * x) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b⁻¹) fun x ↦ x * b
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b⁻¹) ((fun x ↦ x * b) c) = c

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x * b⁻¹) c) = c

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b⁻¹) ((fun x ↦ x * b) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x * b⁻¹) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse (fun x ↦ x⁻¹ * a) fun x ↦ a / x
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ x⁻¹ * a) ((fun x ↦ a / x) c) = c

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a / x) ((fun x ↦ x⁻¹ * a) c) = c

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ x⁻¹ * a) ((fun x ↦ a / x) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a / x) ((fun x ↦ x⁻¹ * a) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b) fun x ↦ x / b

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b) fun x ↦ x / b

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse (fun x ↦ x * b) fun x ↦ x / b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse (fun x ↦ x * b) fun x ↦ x / b
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x / b) c) = c

pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x / b) ((fun x ↦ x * b) c) = c

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x / b) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x / b) ((fun x ↦ x * b) c) = c
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) → ∃ x, x ∈ H ∧ P x

pp: case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) → ∃ x, x ∈ H ∧ P x

case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹