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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l.length) l ++ take (n % l.length) l) (drop (n % l'.length) l' ++ take (n % l'.length) l')

Tactic:
h,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l'.length) l ++ take (n % l'.length) l) (drop (n % l'.length) l' ++ take (n % l'.length) l')
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % min l.length l'.length) (zipWith f l l') ++ take (n % min l.length l'.length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
h,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % min l'.length l'.length) (zipWith f l l') ++ take (n % min l'.length l'.length) (zipWith f l l') =
    drop (n % l'.length) (zipWith f l l') ++ take (n % l'.length) (zipWith f l l')

α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ l.prod

Tactic:
h,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ (s ++ a :: t).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ ((a :: l).rotate n).head? = some a

Tactic:
h,

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l).head? = some a
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate (i % l.length) = l.rotate j

Tactic:
h,

Goal state after:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate (j % l.length) = l.rotate j
Module: Mathlib.Data.List.Rotate

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

Tactic:
· rw [length_cyclicPermutations_of_ne_nil] <;> simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = count y l

Tactic:
h,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun x_1 ↦ (x, x_1)) l) = count y l
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l

Tactic:
h,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, y)) l) = count x l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ n.choose k * k.succ ! * (n - k)! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!

Tactic:
h,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (k + 1) * n ! + n.choose k.succ * k.succ ! * (n - k)! = (n + 1)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
rw [hk₁]; simp [Nat.mul_comm, choose, Nat.sub_self]

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b

Tactic:
h,

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose (a + b - b) = (a + b).choose b
⊢ n.choose a = n.choose b
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
contrapose!; exact nonempty_product

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)

Tactic:
rw [← Nat.mul_left_inj (Nat.mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]
  set p := n - 1
  have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
  simp only [hp, add_succ_sub_one]
  calc
    (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!)
      = (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! := by lia
    _ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
    _ = ((m * (p + 1) + p) + 1)! := by lia
    _ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
    _ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by lia
    _ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
      rw [add_choose_mul_factorial_mul_factorial]
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by lia
    _ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
    _ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by lia

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

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
obtain h | h := Nat.lt_or_ge n k

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ n.descFactorial k = k ! * n.choose k

case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
by
  refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
  rw [← choose_succ_right_eq]
  apply Nat.mul_le_mul_left
  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]
  exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
intro a s ih hs ht
      have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
      have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
      simp only [pi_cons, nodup_bind]
      refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩
      refine (ht a <| mem_cons_self _ _).pairwise ?_
      exact fun b₁ _ b₂ _ neb =>
        disjoint_map_map.2 fun f _ g _ eq =>
          have : Pi.cons s a b₁ f a (mem_cons_self _ _) =
            Pi.cons s a b₂ g a (mem_cons_self _ _) := by rw [eq]
          neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
simp_rw [pi_cons, mem_bind, mem_map, ih]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
hs : s.Infinite
b : β
hb : b ∈ t
⊢ (image2 f s t).Infinite

Tactic:
exact hs.image2_left hb (hfs _ hb)

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ f 1 • b = b

Tactic:
hsmul,

Goal state after:
M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ 1 • b = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f sᶜ = (f '' s)ᶜ

Tactic:
kernImage_eq_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' sᶜᶜ)ᶜ = (f '' s)ᶜ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
kernImage_eq_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ (f '' ∅ᶜ)ᶜ = (range f)ᶜ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
kernImage_eq_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t

Tactic:
kernImage_eq_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t

Tactic:
kernImage_eq_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i ↦ (f i)⁻¹

Tactic:
← image_inv_eq_inv

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (fun x ↦ x⁻¹) '' range f = range fun i ↦ (f i)⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
by
  simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {b * c} = 1

Tactic:
h,

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {1} = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ id '' (s / t) = s * t⁻¹

Tactic:
← image_inv_eq_inv

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ id '' (s / t) = s * (fun x ↦ x⁻¹) '' t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ (s * t)⁻¹ = t⁻¹ * s⁻¹

Tactic:
← image_inv_eq_inv

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ (fun x ↦ x⁻¹) '' (s * t) = (fun x ↦ x⁻¹) '' t * (fun x ↦ x⁻¹) '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (⇑f '' s)⁻¹

Tactic:
← image_inv_eq_inv

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' ⇑f '' s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ n * g ∈ S ↔ g * n ∈ S

Tactic:
h,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ g * (n * g) * g⁻¹ ∈ S ↔ g * n ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑(MulEquiv.refl N)) H = H

Tactic:
MulEquiv.coe_monoidHom_refl,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (MonoidHom.id N) H = H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑(MulEquiv.refl G)) K = K

Tactic:
MulEquiv.coe_monoidHom_refl,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (MonoidHom.id G) K = K
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
A : Type u_4
inst✝¹ : AddGroup A
H : Type u_5
inst✝ : Group H
f : G ≃* H
sg : Subgroup H
⊢ Subgroup.comap (↑f.symm) (Subgroup.comap (↑f) sg) = sg

Tactic:
simp [Subgroup.comap_comap]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
A : Type u_4
inst✝¹ : AddGroup A
H : Type u_5
inst✝ : Group H
f : G ≃* H
sh : Subgroup G
⊢ Subgroup.comap (↑f) (Subgroup.comap (↑f.symm) sh) = sh

Tactic:
simp [Subgroup.comap_comap]

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f x * f y⁻¹ = 1

Tactic:
h,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f y * f y⁻¹ = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f y⁻¹ * f x = 1

Tactic:
h,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f y⁻¹ * f y = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x ∈ f.ker
⊢ x = y

Tactic:
h,

Goal state after:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x ∈ ⊥
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
K L : Subgroup N
⊢ comap f K = comap f L → K = L

Tactic:
by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) ↔ ∃ y z, ↑y * ↑z = x

Tactic:
by simp only [SetLike.exists, exists_prop]

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
P : C → Prop
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
grind [mem_sup]

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
ι : Type u_5
f : F
hf : Injective ⇑f
S : Submonoid M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
by simp [mem_comap, mem_map, hf.eq_iff]

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

Goal state before:
pp: m n : ℕ
⊢ max m n ^ 2 + min m n ≤ pair m n

Tactic:
pair

Goal state after:
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
A : Type u_4
inst✝¹ : AddGroup A
H✝ K : Subgroup G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Characteristic
⊢ (⨅ i, H i).Characteristic

Tactic:
simp_all [characteristic_iff_comap_eq, comap_iInf]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
f : F
⊢ x • graphOn (⇑f) univ = graphOn (fun a ↦ x.2 / f x.1 * f a) univ

Tactic:
simp [smul_graphOn]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
by
  rw [closure_singleton_eq, mem_mrange]; rfl

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hx', hs x hx]

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p (k - 1 + 1)

Tactic:
by rwa [Nat.sub_add_cancel this]

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)

Tactic:
simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]

Goal state after:
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.comp f₁) a = g (f₂ a)

Tactic:
h,

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.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
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: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
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: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ f a ⊓ f b = ⊥

Tactic:
← map_inf,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ f (a ⊓ b) = ⊥