mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
by
  simp_rw [mem_uIcc]
  exact Set.eq_of_mem_uIcc_of_mem_uIcc

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
⊢ False

Tactic:
obtain ⟨m, n, mn, hmn⟩ := hf' fun n x hx => by
    split_ifs at hx with hn
    exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]

Goal state after:
case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
⊢ False
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M

Tactic:
by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: case zero
α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x ↦ f x ^ 0) ⊆ mulSupport f

Tactic:
simp [pow_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: case succ
α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x ↦ f x ^ (n + 1)) ⊆ mulSupport f

Tactic:
simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, ⁅h, g⁆ = 1

Tactic:
by
  simp only [commutatorElement_def, mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
hx : x ∈ closure s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
by
    classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤

Tactic:
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]
  refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)
  rw [Quot.eq]
  simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
x✝¹ x✝ : M
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝

Tactic:
apply H

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂

Tactic:
by
  simp +contextual [Step.cons_left_iff, iff_def, or_imp]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ : List (α × Bool)
⊢ (invRev L₁).length = L₁.length

Tactic:
simp [invRev]

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
⊢ invRev (L₁ ++ L₂) = invRev L₂ ++ invRev L₁

Tactic:
simp [invRev]

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a : α × Bool
⊢ invRev (a :: L) = invRev L ++ invRev [a]

Tactic:
simp [invRev]

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

Goal state before:
pp: case not
α : Type u
L L₁ L₂ L₃ L₄ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (invRev (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (invRev (L₁✝ ++ L₂✝))

Tactic:
simp [invRev]

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

Goal state before:
pp: α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (Quot.mk Red.Step tl)⁻¹ * Quot.mk Red.Step tl = 1
x : α
b : Bool
⊢ Red.Step (invRev ((x, b) :: tl) ++ (x, b) :: tl) (invRev tl ++ tl)

Tactic:
simp [invRev]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1

Tactic:
exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Monoid M
s : Finset M
⊢ FG ↥(Submonoid.closure ↑s)

Tactic:
by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid

Tactic:
exact (Subgroup.closure_toSubmonoid _).symm

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ ↑(a / b) = 1

Tactic:
simp only [h, QuotientGroup.mk_div, div_self']

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ z * y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
apply mul_mem

Goal state after:
case neg.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ z ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

case neg.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (lift (g ∘ f)) x = (lift g) ((map f) x)

Tactic:
induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
⊢ f x⁻¹ ≤ g x⁻¹ ↔ g x ≤ f x

Tactic:
by
  suffices h : ∀ (f g : F) (x), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x from
    ⟨h f g x, by simpa using h g f x⁻¹⟩
  exact fun f g x hfg ↦ calc
    _ = f x * (f x⁻¹ * g x) := by simp [← mul_assoc, ← map_mul]
    _ ≤ f x * (g x⁻¹ * g x) := by gcongr
    _ = f x                 := by simp [← map_mul]

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {x y z : M × ↥S},
    (∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑z.2 * x.1) = ↑c * (↑x.2 * z.1)

Tactic:
rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩

Goal state after:
case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ∃ c_1, ↑c_1 * (↑c.2 * a.1) = ↑c_1 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
exact mulEquivOfQuotient_mk' _ _

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

Goal state before:
pp: case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b

pp: case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝ * b) = untopD 0 ↑a✝ * untopD 0 b

Tactic:
· rw [top_mul hb, untopD_top, zero_mul]

Goal state after:
case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝ * b) = untopD 0 ↑a✝ * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥ * ↑x
⊢ a < ⊥

Tactic:
bot_mul x0'

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥
⊢ a < ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn

Tactic:
simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
exact ⟨_, hm', hm⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : succ a < b
⊢ (Ioo a b).Nonempty

Tactic:
exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise f (update g i v)

Tactic:
rw [update_piecewise]
  refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl
  exact fun h => hi (h ▸ hj)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
Finset.prod_dite,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = (∏ x, f ⟨↑x, ⋯⟩) * ∏ x, 1
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
x✝ : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)

Tactic:
by
    classical exact (Equiv.sumCompl (· = a)).bijective

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

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
rw [if_pos h, if_neg h, add_zero]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]
    convert! s.attach_map_coe

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

Goal state before:
pp: case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (set ⟨val✝², property✝⟩ ⟨val✝¹, isLt✝¹⟩ a).get ⟨val✝, isLt✝⟩ = get ⟨val✝², property✝⟩ ⟨val✝, isLt✝⟩

Tactic:
simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]

Goal state after:
case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (val✝².set val✝¹ a)[val✝] = val✝²[val✝]
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a ↔ ∃ a' < a, f a' = b

Tactic:
by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_rel h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.lt_iff_lt] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.strictMono hc

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

Goal state before:

Tactic:
f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
h.toOption,

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = (Option.some (o.get h)).elim Option.none fun a ↦ (f a).toOption
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) → p ∧ ∃ h, o.get h = a

Tactic:
rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : c i = some a
⊢ a = b

Tactic:
obtain ⟨j, hb⟩ := hb

Goal state after:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : some b = c j
⊢ a = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) → some x ∈ c

Tactic:
exact fun a ↦ mem_chain_of_mem_ωSup a

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ ∀ (a b : Cardinal.{u}), a ≤ b ∨ b ≤ a

Tactic:
by
      rintro ⟨α⟩ ⟨β⟩
      apply Embedding.total

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
e : β ↪ ULift.{v, u} α
⊢ #β ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
replace e := e.congr (Equiv.refl β) Equiv.ulift

Goal state after:
case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
e : β ↪ α
⊢ #β ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ ↑(n + 1) = c ^ ↑n * c

Tactic:
cast_succ,

Goal state after:
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ (↑n + 1) = c ^ ↑n * c
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b

Tactic:
rw [← smul_eq_mul] at ab

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
h' : #↑(T \ S) = 0
⊢ #↑(T \ S) + #↑S ≤ #↑S

Tactic:
by simp [h']

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_2
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = lift.{u, u} #↑(f ⁻¹' s)

Tactic:
rw [lift_id]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_3
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑s = lift.{u, u} #↑s

Tactic:
rw [lift_id]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x : α
⊢ #α = 2 ↔ ∃! y, y ≠ x

Tactic:
rw [mk_eq_two_iff]

Goal state after:
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ ((↑e).inverse e.invFun ⋯ ⋯) (r • x) = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x

Tactic:
by rw [map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
c : R
x : M
⊢ f (c • x) = σ c • f x

Tactic:
by rw [map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid V
inst✝¹³ : Module R V
inst✝¹² : Module S V
inst✝¹¹ : AddCommMonoid W
inst✝¹⁰ : Module R W
inst✝⁹ : Module S W
inst✝⁸ : AddCommMonoid G
inst✝⁷ : Module R G
inst✝⁶ : Module S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ (α • e) ≪≫ₗ f = α • e ≪≫ₗ f

Tactic:
ext; simp [LinearMapClass.map_smul_of_tower f]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (f (m • x)) = g (φ m • f x)

Tactic:
by rw [map_smulₛₗ]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (φ m • f x) = ψ (φ m) • g (f x)

Tactic:
by rw [map_smulₛₗ]

Goal state after: