mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
hs : s ≠ 0
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

Tactic:
by
  induction s using Quotient.inductionOn; aesop (add simp List.prod_hom₂_nonempty)

Goal state after:
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.Nat.Choose.Basic

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

Tactic:
succ_sub (le_of_lt_succ hk₁),

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k.succ).succ ! = (n - k.succ).succ * (n - k.succ)!
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s

Tactic:
simp [mem_image, ht.exists_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t

Tactic:
simp [mem_image, ht.exists_mem]

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

Goal state before:
pp: case mem.mul
M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x✝ y✝ : M
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p z x✝ ⋯ hx✝
h₂ : p z y✝ ⋯ hy✝
⊢ p z (x✝ * y✝) ⋯ ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
← closure_singleton_le_iff_mem,

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ closure {m} ≤ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

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
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

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

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
N N' : Submonoid M
⊢ N ⊔ N' = closure (↑N ∪ ↑N')

Tactic:
by
  simp_rw [closure_union, closure_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
← closure_singleton_le_iff_mem,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ closure {m} ≤ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
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 α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 ↦ x1 / x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s / t)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H H' : Subgroup G
⊢ H ⊔ H' = closure (↑H ∪ ↑H')

Tactic:
by
  simp_rw [closure_union, closure_eq]

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✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
⊢ IsMulCommutative ↥(map f H)

Tactic:
refine .of_setLike_mul_comm ?_
  rintro - ⟨a, ha, rfl⟩ - ⟨b, hb, rfl⟩
  simpa [map_mul] using congr(f $(setLike_mul_comm ha hb))

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 : y⁻¹ * x ∈ f.ker
⊢ f y * f (y⁻¹ * x) = f y

Tactic:
mem_ker.1 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 : y⁻¹ * x ∈ f.ker
⊢ f y * 1 = f y
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a * a = q * a * a

Tactic:
eq,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a * a = 1 * a
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
· rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ (B' ⊓ B))

Tactic:
exact le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
let := ofEquiv _ e
  refine ofNat_of_decode ?_
  rw [decode_ofEquiv e]
  simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝¹ : DecidablePred fun x ↦ x ∈ Set.range encode := decidableRangeEncode α
this✝ : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (⇑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
this : Denumerable ↑(Set.range encode) := Subtype.denumerable (Set.range encode)
⊢ Denumerable α

Tactic:
exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
revzip_powersetAux_lemma l revzip_powersetAux,

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l - x)) (powersetAux l) ~ (powersetAux' l).revzip
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists ~ l.sublists'

Tactic:
rw [← map_get_finRange l, sublists_map, sublists'_map]

Goal state after:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (x ⊆ t ∧ #x = n) ∧ s ⊆ x → ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

Tactic:
intro ⟨⟨hxt, hxn⟩, hsx⟩
    exact ⟨x \ s, ⟨fun y hy => mem_sdiff.mpr ⟨hxt (mem_sdiff.mp hy).1, (mem_sdiff.mp hy).2⟩,
           by rw [card_sdiff_of_subset hsx, hxn]⟩, sdiff_union_of_subset hsx⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Tactic:
· exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

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

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

Tactic:
| cons _ _ _ _ ih =>

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

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

Tactic:
| cons _ _ _ _ ih =>

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (sSup (range fun i ↦ f i)) = ⨆ i, l (f i)

Tactic:
gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ ⨆ x, l ↑x = ⨆ i, l (f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sSup ↑s ∈ s

Tactic:
rw [h.csSup_eq_max']
  exact s.max'_mem _

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ x, ∀ y ∈ range fun c ↦ f (b, c), y ≤ x

Tactic:
exact ⟨B, by grind⟩

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)

Tactic:
· rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ #(sigmaLift f a b) = if h : a.fst = b.fst then #(f (h ▸ a.snd) b.snd) else 0

Tactic:
by
  simp_rw [sigmaLift]
  split_ifs with h <;> simp

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f i ≤ f j
this : ¬f j ≤ f i
⊢ False

Tactic:
exact h.not_lt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
by
  rw [sInf_eq_zero]
  right
  rfl

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
classical
    let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
    by_cases hbad : Infinite bad
    · refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
    · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ WellFoundedGT α

Tactic:
· rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
    refine ⟨fun a => ?_⟩
    obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
    exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
Set.Icc_subset_Ioo_iff h₁

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ a₂ < a₁ ∧ b₁ < b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
⊢ ¬a < b

Tactic:
intro h
  induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih
  subst hs
  obtain ⟨c, hac, hcb⟩ := exists_between h
  refine ih _ ?_ c hac rfl
  exact Finset.Icc_ssubset_Icc_right (hac.trans hcb).le le_rfl hcb

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
Set.Icc_eq_singleton_iff

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a = c ∧ b = c ↔ a = c ∧ b = c
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • (a✝ * b✝) = a✝ * b✝

Tactic:
smul_mul',

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • a✝ * x✝ • b✝ = a✝ * b✝
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • (↑x * y) = ↑x * g • y

Tactic:
smul_mul',

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • ↑x * g • y = ↑x * g • y
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ g⁻¹ • a ∈ U

Tactic:
rw [← hu₂]

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ g⁻¹ • (fun x ↦ g • x) u ∈ U
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : x ∈ ⨆ i, S i), C x h

Tactic:
refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : G
hx : x ∈ S i
⊢ ∃ (h : x ∈ ⨆ i, S i), C x h

case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

Tactic:
by
  split_ifs with h <;> rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
⊢ (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

Tactic:
by
  split_ifs with h <;> rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ t.noncommProd f comm ∈ S

Tactic:
by
  apply multiset_noncommProd_mem
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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

Goal state before:
pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i

pp: case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1

Tactic:
· simp only [Pi.mulSingle_eq_same]

Goal state after:
case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
constructor
  · generalize hL : ((a, b) :: L₁ : List _) = L
    rintro @⟨_ | ⟨p, s'⟩, e, a', b'⟩ <;> simp_all
  · rintro (⟨L, h, rfl⟩ | rfl)
    · exact Step.cons h
    · exact Step.cons_not

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case e'_3
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : β = Multiplicative β
⊢ f x = (FreeGroup.lift f) (FreeGroup.of x)

Tactic:
exact (FreeGroup.lift_apply_of (β := Multiplicative β)).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p

Tactic:
rw [map_pure, pure_seq]
      induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
have h₀ := ore_eq r₁ s₂

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = oreNum r₁ s₂ * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
⊢ ∃ z' w' d, z * f ↑d = f z' ∧ w * f ↑d = f w'

Tactic:
by
  let ⟨a, ha⟩ := surj f z
  let ⟨b, hb⟩ := surj f w
  refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩
  · simp_rw [mul_def, map_mul, ← ha]
    exact (mul_assoc z _ _).symm
  · simp_rw [mul_def, map_mul, ← hb]
    exact mul_left_comm w _ _

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
inj : Injective ⇑k
⊢ z = w

Tactic:
apply (f.map_units x).mul_right_cancel
    rw [hxz, hxw, hg (inj this)]

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁵ : Mul R
inst✝⁴ : Add R
inst✝³ : Mul S
inst✝² : Add S
inst✝¹ : Preorder R
inst✝ : Preorder S
e : R ≃+*o S
x : R
y : S
⊢ x < e.symm y ↔ e x < y

Tactic:
by
  simpa using! e.toOrderIso.lt_symm_apply

Goal state after: