mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝³ : CommGroup G
inst✝² : PartialOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
x y : Gᵒᵈ
hy✝ : 1 < y
hy : ofDual y < 1
n : ℕ
hn : (ofDual x)⁻¹ ≤ (ofDual y)⁻¹ ^ n
⊢ x ≤ y ^ n

Tactic:
rwa [inv_pow, inv_le_inv_iff] at hn

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉

Tactic:
add_one_le_iff,

Goal state after:
case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌊a⌋ < ⌈a⌉
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • 1 = 1

Tactic:
← f.map_one,

Goal state after:
G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • f 1 = f 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑z + 1 < y * ↑n

Tactic:
grw [(zh _).1 le_rfl]

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x * ↑n + 1 < y * ↑n
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
b : H
f : G →+c[a, b] H
x✝ : G
⊢ -f (-(x✝ + a)) = -f (-x✝) + b

Tactic:
simp [neg_add_eq_sub]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x y : WithBot M
⊢ 0 < y → ∃ n, x ≤ n • y

Tactic:
hxy

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x y : WithBot M
hxy : 0 < y
⊢ ∃ n, x ≤ n • y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x y : WithZero M
⊢ 1 < y → ∃ n, x ≤ y ^ n

Tactic:
hxy

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x y : WithZero M
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
refine (Nat.sub_eq_of_eq_add ?_).symm
  rw [← countP_append]
  exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

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

Goal state before:
pp: α : Type u_1
s : Multiset α
e : s = 0
⊢ s.card = 0

Tactic:
simp [e]

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

Goal state before:
pp: α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a

Tactic:
by rw [← replicate_le_coe, coe_replicate]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ range l.get = {x | x ∈ l}

Tactic:
ext x
  rw [mem_ofPred_eq, mem_iff_get, mem_range]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : β → α → β
inst✝ : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f x s)

Tactic:
by
  rw [foldl_swap]
  exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b ↦ f a = f b) s t ↔ Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
simp only [hf.eq_iff]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
· simpa [h] using cons_le_cons a (IH (t := t.erase a))

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Tactic:
by
  rw [d.erase_eq_filter b, mem_filter, and_comm]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ take l₁.length (l₂ ++ l₃) = take l₁.length l₂

Tactic:
take_eq_left_iff

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y

Tactic:
nth_rw 1 [List.prefix_iff_eq_take.mp h]

Goal state after:
case h
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
x✝ : α
⊢ ¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
Classical.not_imp,

Goal state after:
α : Type u_2
s t : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ ¬x✝ ∉ t ↔ x✝ ∈ s ∧ x✝ ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f (image f^[n] s) = image (f ∘ f^[n]) s

Tactic:
image_image

Goal state after:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image (f ∘ f^[n]) s = image (f ∘ f^[n]) s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < last (n + 1)

Tactic:
rw [lt_def, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ n ≠ 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j

Tactic:
exact castSucc_injective _ hij

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = #s

Tactic:
rw [← subtype_card s H]
  congr!

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) i = snoc (f ∘ natAdd m) a i

Tactic:
refine Fin.lastCases ?_ (fun i ↦ ?_) i

Goal state after:
case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) (last n) = snoc (f ∘ natAdd m) a (last n)

case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) i.castSucc = snoc (f ∘ natAdd m) a i.castSucc
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
by
  induction n generalizing s with
  | zero => exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
  | succ n IH =>
    rcases hn.eq_or_lt with hn' | hn'
    · exact ⟨s, subset_rfl, hn'⟩
    obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
    obtain ⟨x, hx⟩ := exists_notMem_finset t
    refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
    simp [ht]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s : Finset α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x ↦ c) s = if s = ∅ then b else op b c

Tactic:
induction s using Finset.induction_on generalizing hd with

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α

Tactic:
nontriviality α
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩
  simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ ((r c b ∨ r c (f a)) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
or_assoc

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)

pp: case refine_1.inr
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)

Tactic:
· exact Lex.rel h

Goal state after:
case refine_1.inr
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod

Tactic:
prod_eq_foldr

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun x1 x2 ↦ x1 * x2) 1 s)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate (n % (a :: l).length)).prod = 1

Tactic:
rotate_eq_drop_append_take this,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
eq_nil_of_length_eq_zero hl.symm,

Goal state after:
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = [] ↔ l.rotate n = [].rotate ((([].length - n % [].length) % [].length + n % [].length) % [].length)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ (map f m).prod = f i ^ count i m

Tactic:
induction m using Quotient.inductionOn

Goal state after:
case h
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
i : ι
a✝ : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a✝⟧ → f i' = 1
⊢ (map f ⟦a✝⟧).prod = f i ^ count i ⟦a✝⟧
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = ↑(l₁.product l₂)

Tactic:
List.product,

Goal state after:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = ↑(List.flatMap (fun a ↦ List.map (Prod.mk a) l₂) l₁)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j * i ! * j ! = (i + j)!

Tactic:
by
  rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
    Nat.mul_right_comm]

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

Goal state before:
pp: n : ℕ
⊢ n.multichoose 0 = 1

Tactic:
cases n <;> simp [multichoose]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x✝ : α
⊢ x✝ ∈ iUnion (Fin.cons s f) ↔ x✝ ∈ s ∪ ⋃ i, f i

Tactic:
simp [Fin.exists_iff_succ]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
rintro (h | h)

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite
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
⊢ 1 • b = b

Tactic:
← f.map_one,

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
⊢ f 1 • b = b
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑((Units.map f) c)) (f a) (f b)

Tactic:
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]

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)
x : α
hx : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
⊢ f x = f y → x = y

Tactic:
hxy

Goal state after:
α : 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)
x : α
hx : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
⊢ x = y
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
rw [pow_succ]; exact hs.pow.mul hs

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

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
⊢ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x

Tactic:
ext ⟨_, _⟩
  simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]; tauto

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
· rintro ⟨b, c, rfl, rfl, h⟩
    rw [singleton_mul_singleton, h, singleton_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
by
  simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ S

Tactic:
ha (a⁻¹ * n * a⁻¹⁻¹)

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1}) = closure s

Tactic:
by
  rw [← closure_union_one (s \ {1}), sdiff_union_self, closure_union_one]

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

Goal state before:
pp: case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
· exact ⟨1, s.one_mem, y, h, by simp⟩

Goal state after:
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 K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)

Tactic:
inf_eq_right.mpr hK,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ H ⊔ K = f.range ⊓ (H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
⊢ (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y → x = y

Tactic:
hxy

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y
⊢ x = y
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 : Surjective ⇑f
S : Submonoid N
x : N
h : x ∈ S
y : M
hy : f y = x
⊢ y ∈ comap f S ∧ f y = x

Tactic:
by simp [hy, h]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

Tactic:
by
  cases n using bitCasesOn with
  | bit b n => cases b <;>
    simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

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

Goal state before:
pp: case neg
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
hl : n - s * s - s ≤ s
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n

Tactic:
simp [s, pair, hl.not_gt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]

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

Goal state before:
pp: case h
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a

Tactic:
exact Nat.add_le_add_left (le_of_not_gt h) _

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

Goal state before:
pp: case false
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match false, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

Tactic:
simp [e]

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

Goal state before:
pp: case true
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match true, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

Tactic:
simp [e]

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

Goal state before:
pp: α : Type u_1
a : FreeMonoid α
⊢ a.reverse.reverse = a

Tactic:
apply List.reverse_reverse

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
simp_rw [Set.smul_set_inter, smul_mul_assoc]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h₂ : f i < g i ∨ ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
cases h₂

Goal state after:
case cons.inl
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h).range ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Tactic:
MonoidHom.range_eq_map

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}
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.prod = 1

Tactic:
by
    rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
    · exact (length l)
    · rfl

Goal state after: