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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
· simp [h, mt p.mem_iff.2 h, IH p]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
erase_of_notMem m

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p s - filter p t = filter p s - filter p t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩

Tactic:
by
  simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
  rw! [Finset.union_symm_right h hi hi']
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
p : α → Prop
inst✝ : DecidablePred p
⊢ map f.toEmbedding (filter p s) = filter (p ∘ ⇑f.symm) (map f.toEmbedding s)

Tactic:
simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
⊢ (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) =
    s

Tactic:
by
    ext a; constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding] at * <;>
    grind

Goal state after:
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
h : Nonempty (Fin (n + 1) ↪ Fin m)
⊢ n + 1 ≤ m

Tactic:
obtain ⟨e⟩ := h

Goal state after:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
⊢ n + 1 ≤ m
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
constructor
  · intro hf i hi
    have := hf hi
    simp [Fin.ext_iff] at this
  · intro hf
    refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective
    exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hab : b ≤ a
⊢ a - b ≠ last n

Tactic:
by
  rw [← lt_last_iff_ne_last, lt_def]
  exact val_sub_lt_of_lt_of_le (val_lt_last ha) hab

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

Tactic:
split <;> fin_omega

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≠ p

Tactic:
rcases p.castSucc_lt_or_lt_succ i with (h | h)
  · rw [succAbove_of_castSucc_lt _ _ h]
    exact Fin.ne_of_lt h
  · rw [succAbove_of_lt_succ _ _ h]
    exact Fin.ne_of_gt h

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ a.succAbove 0 = 0

Tactic:
Fin.succAbove_of_castSucc_lt

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i

Tactic:
by
  rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), castPred_castSucc]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
by
  rw [one_lt_card]
  simp only [exists_and_left]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬(↑s).Nontrivial

Tactic:
← Set.nontrivial_coe_sort,

Goal state after:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬Nontrivial ↑↑s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = cons (x₀ 0) x (Fin.cast ⋯ (natAdd 1 i))

Tactic:
Fin.cast_natAdd,

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = cons (x₀ 0) x (i.addNat 1)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
simp only [comp_apply, snoc_castSucc]
    rw [natAdd_castSucc, snoc_castSucc]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
z : α (last n)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc xs x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.snoc (init x) (x (last n))) = motive x

Tactic:
by rw [Fin.snoc_init_self]

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

Goal state before:
pp: case h.h₂
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ #s ≤ #(map f univ)

Tactic:
· simp [← hsn]

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

Goal state before:
pp: case mp.cons_cons.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?

Tactic:
simpa using hf _

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩

Goal state after:
case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = l.get (f ⟨0, ⋯⟩) ∧ x = l.get (f ⟨1, ⋯⟩)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ motive s hs

Tactic:
lift s to Finset α using hs
  induction s using Finset.cons_induction_on with
  | empty => simpa
  | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
i : Fin n
y : α (p.succAbove i)
f : (j : Fin n) → α (p.succAbove j)
⊢ p.insertNth x (update f i y) = update (p.insertNth x f) (p.succAbove i) y

Tactic:
by
  simp [insertNth_eq_iff]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
· exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

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:
classical
    induction s using Finset.induction_on generalizing hd with
    | empty => simp
    | insert x s hx IH =>
      simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ decide (r x✝² x✝¹) = true → decide (r x✝¹ x✝) = true → decide (r x✝² x✝) = true

Tactic:
simpa using trans_of r

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
n : ℕ
⊢ ∃ s, #s = n + 1

Tactic:
obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩

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

Goal state before:
pp: α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
cases eq_nil_or_concat l with grind

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

Tactic:
ext x
  rcases lt_trichotomy (x : ℕ) j with (h | h | h)
  · simp only [Function.comp_apply, contractNth_apply_of_lt, h]
  · simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]
  · simp only [Function.comp_apply, contractNth_apply_of_gt, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  change _ ≤ _ ↔ _
  exact max_le_iff

Goal state after:
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
⊢ (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1

Tactic:
mul_eq_one_iff_inv_eq,

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)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ a ^ (-1) ^ l.length / l.alternatingProd ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length

Tactic:
div_zpow

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ a ^ (-1) ^ l.length / l.alternatingProd ^ (-1) ^ l.length = a ^ (-1) ^ l.length / l.alternatingProd ^ (-1) ^ l.length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (Disjoint on f) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
unfold Function.onFun

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (fun x y ↦ Disjoint (f x) (f y)) (Quot.mk (⇑(List.isSetoid α)) a)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t

Tactic:
by simp [SProd.sprod, product, and_left_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
refine s.induction ?_ ?_
  · simp
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]

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

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup

Tactic:
rw [nodup_iff_injective_get]
    rintro ⟨i, hi⟩ ⟨j, hj⟩ h
    simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
    simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h

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

Goal state before:
pp: ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
⊢ Infinite ((i : ι) → π i)

Tactic:
let ⟨m⟩ := @Pi.instNonempty ι π _

Goal state after:
ι : Sort u_4
π : ι → Sort u_5
i : ι
inst✝¹ : Infinite (π i)
inst✝ : ∀ (i : ι), Nonempty (π i)
m : (a : ι) → π a
⊢ Infinite ((i : ι) → π i)
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(image (const ι) s) = #s

Tactic:
card_image_of_injective _ const_injective

Goal state after:
α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #s = #s
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ f a ∈ t a

Tactic:
rw [← hgf]

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g a ∈ t a
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : a ∈ Set.ofPred IsUnit
hb : b ∈ Set.ofPred IsUnit
⊢ a * b ∈ Set.ofPred IsUnit

Tactic:
rw [Set.mem_ofPred_eq] at *

Goal state after:
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a b : M
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b)
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
x y : G
h : x ∈ H
hba : y * x ∈ H
⊢ y ∈ H

Tactic:
by simpa using mul_mem hba (inv_mem h)

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

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹

Tactic:
exact ⟨-n, zpow_neg x n⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = K ↔ K ≤ H

Tactic:
inf_eq_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ↔ K ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ ∀ (a : G₁), f a = K.subtype k ↔ (f.codRestrict K ⋯) a = k

Tactic:
simp [Subtype.ext_iff]

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✝
H : Type u_6
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup G
h :
  { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2

Tactic:
by simpa [Subgroup.map_map] using
      Subgroup.map_mono (f := (f.symm : H →* G)) h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
⊢ x ∈ iSup K ↔ ∃ i, x ∈ K i

Tactic:
by
  have : iSup K = ⨆ i : PLift ι, ⨆ (_ : True), K i.down := by simp [iSup_plift_down]
  rw [this, mem_biSup_of_directedOn trivial]
  · simp
  · simp only [ofPred_true]
    rw [directedOn_onFun_iff, Set.image_univ, directedOn_range]
    -- `Directed.mono_comp` and much of the Set API requires `Type u` instead of `Sort u`
    intro i
    simp only [PLift.exists]
    intro j
    refine (hK i.down j.down).imp ?_
    simp
  · exact PLift.up hι.some

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 : Subgroup N
h : H ≤ f.range
⊢ f.range ⊓ H = H

Tactic:
inf_eq_right

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
h : H ≤ f.range
⊢ H ≤ f.range
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:
by
  grind [mem_sup]

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 G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ H = K

Tactic:
apply_fun comap f at hf

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

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

Tactic:
Subgroup.closure_union,

Goal state after:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x} ⊔ closure {y} ↔ ∃ m n, x ^ m * y ^ n = z
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
by
  rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
by
  rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

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

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

pp: case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
· show unpair (b * b + a) = (a, b)
    have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
    simp [unpair, be, Nat.add_sub_cancel_left, h]

Goal state after:
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
by
  rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

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

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
exact Lex.right _ _ (symm hab)

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

Goal state before:
pp: case inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ 1 ∈ powers a

pp: case inr
M : Type u_1
inst✝ : Monoid M
x✝ : M
ha : IsIdempotentElem x✝
S : Submonoid M := { carrier := {1, x✝}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ x✝ ∈ powers x✝

Tactic:
exacts [one_mem _, Submonoid.mem_powers _]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
hne : x ≠ y
U : Set α
hU : U ∈ s
hSU : S ⊆ U
hTU : T ⊆ U
⊢ r x y

Tactic:
exact h U hU (hSU hx) (hTU hy) hne

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : ∀ b ∈ cons a✝ s✝ h✝, p (f b)
⊢ p ((cons a✝ s✝ h✝).sup f)

Tactic:
simp only [sup_cons, forall_mem_cons] at hs ⊢

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
p : α → Prop
hb : p ⊥
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : (∀ b ∈ s✝, p (f b)) → p (s✝.sup f)
hs : p (f a✝) ∧ ∀ x ∈ s✝, p (f x)
⊢ p (f a✝ ⊔ s✝.sup f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ a \ f a✝ ⊔ a \ s✝.inf f = a \ (f a✝ ⊓ s✝.inf f)

Tactic:
sdiff_inf

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ a \ f a✝ ⊔ a \ s✝.inf f = a \ f a✝ ⊔ a \ s✝.inf f
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b ↦ f b \ a) = s.inf f \ a

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [inf_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [inf_cons, inf_cons, ih, inf_sdiff]

Goal state after: