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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝² : CommMonoid M
f : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = (∏ x ∈ s with p x ∧ ¬q x, f x) * ∏ x ∈ s with q x ∧ ¬p x, f x

Tactic:
classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
  simp only [Xor]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ FG M ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ

Tactic:
by
  refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
  · rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]
  · rintro ⟨S, hfin : Finite S, φ, hφ⟩
    refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩
    simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
exact ih _ hz₂ hz₃ hz₁.le hz₁.not_ge

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
⊢ k • (count x s / k) • {x} = count x s • {x}

Tactic:
rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
⊢ x * y * 0 = x * (y * 0)

Tactic:
simp only [mul_zero]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ g : α →*o β
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
monotone'✝ : Monotone (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g : α →*o β
toFun✝¹ : α → β
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun x * { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun y
monotone'✝¹ : Monotone (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
monotone'✝ : Monotone (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, monotone' := monotone'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ g : α →*₀o β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
monotone'✝ :
  Monotone (↑{ toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝,
        monotone' := monotone'✝ } =
    (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } =
    g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀o β
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun x * { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun y
monotone'✝¹ :
  Monotone (↑{ toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
monotone'✝ :
  Monotone (↑{ toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹,
        monotone' := monotone'✝¹ } =
    (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝,
        monotone' := monotone'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹,
      monotone' := monotone'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ }
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ 1 = mk (↑a) a

Tactic:
rw [← mk_one, mk_eq_mk_iff]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S
⊢ (r S) (1, 1) (↑a, a)
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
x y : M
c : ↥S
h : f (↑c * x) = f (↑c * y)
⊢ f x = f y

Tactic:
by
  rw [map_mul, map_mul] at h
  let ⟨u, hu⟩ := f.map_units c
  rw [← hu] at h
  exact (Units.mul_right_inj u).1 h

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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

Tactic:
simp only [mul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ a ^ (n + 1) = a ^ n * a

Tactic:
by simp_rw [HPow.hPow, Pow.pow]; cases n <;> cases a <;> simp [pow_succ]

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

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

pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * a < ↑x * ↑a✝
⊢ a < ↑a✝

Tactic:
· rw [mul_bot x0'] at h
      exact absurd h bot_le.not_gt

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a

Tactic:
have := mem_range_succ_or_isSuccPrelimit a

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
this : a ∈ range succ ∨ IsSuccPrelimit a
⊢ IsMin a ∨ a ∈ range succ ∨ ¬IsMin a ∧ IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ (prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) = isMin b hb

Tactic:
prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ (if h : IsMin b then isMin b h
    else
      isSuccLimit b ⋯ fun x x_1 ↦
        prelimitRecOn x succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isMin b hb
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (if h : IsMin b then isMin b h
    else
      isSuccLimit b ⋯ fun x x_1 ↦
        prelimitRecOn x succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Tactic:
by
  simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)

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

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
rw [pred_eq_iff_isMin.2 ha']
      exact hn this

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

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
rw [pred_eq_iff_isMin.2 ha']
      exact hn this

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✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Tactic:
rw [prod_eq_mul_prod_sdiff_singleton_of_mem h, mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i ↦ b ↑i) univ ⊂ image b univ

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
⊢ m.card = n

Tactic:
apply_fun Multiset.card at h

Goal state after:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : (↑s).card = (a ::ₘ m).card
⊢ m.card = n
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]

Tactic:
by
  rw [← v.cons_head_tail]
  simp only [toList_cons, toList_nil, head_cons, singleton_tail]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ (map id v).toList = v.toList

Tactic:
by simp only [List.map_id, Vector.toList_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
x✝¹ x✝ : { x // x.length = 1 }
val✝¹ : List α
property✝ : val✝¹.length = 1
val✝ : List α
h : val✝.length = 1
perm : ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩
⊢ (↑⟨val✝¹, property✝⟩).head ⋯ = (↑⟨val✝, h⟩).head ⋯

Tactic:
by
      obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h
      exact List.eq_of_mem_singleton (List.Perm.mem_iff perm |>.mp <| List.head_mem _)

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
⊢ #({f ∈ piFinset s | f i = a}) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Tactic:
by
  split_ifs with h
  · rw [card_filter_piFinset_eq_of_mem _ _ h]
  · rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ b, a < b

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i ↦ f (i + 1)

Tactic:
simp only [mk_sum, mk_out, lift_id, mk_sigma]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s

Tactic:
by
  simp [IsUpperSet, subset_def, @forall_comm (_ ∈ s)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑↑f '' s)

Tactic:
rw [Equiv.image_eq_preimage_symm]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x ↦ (f x).bind (g x)

Tactic:
rintro x y h a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x ↦ (f x).bind (g x)) x → a ∈ (fun x ↦ (f x).bind (g x)) y
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
⊢ Antitone fun x ↦ (f x).bind (g x)

Tactic:
rintro x y h a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x ↦ (f x).bind (g x)) y → a ∈ (fun x ↦ (f x).bind (g x)) x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x

Tactic:
constructor
  · rw [Ne, eq_none_iff', not_not]
    exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
  · rintro ⟨x, rfl⟩
    apply some_ne_none

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b

Tactic:
simp [inter_def]; aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

Tactic:
simp [inter_def]; aesop

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

Goal state before:
pp: α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift '' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})

Tactic:
rw [Equiv.image_eq_preimage_symm]

Goal state after:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Tactic:
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
simpa using lift_le (b := ℵ₀)

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ a = ↑n

Tactic:
nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt]

Goal state after:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ ↑(toNat a) = ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]
    | inr hy =>
      simp only [toENatAux_eq_top hy, add_top]
      exact toENatAux_eq_top <| le_add_left hy

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

Goal state before:
pp: n : ℕ
h : IsSuccLimit ↑n.succ
⊢ False

Tactic:
rw [Nat.cast_succ, ← succ_natCast] at h
    exact Order.not_isSuccLimit_succ _ h

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

Goal state before:
pp: α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]

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

Goal state before:
pp: n : ℕ
⊢ ↑n + ℵ₀ = ℵ₀

Tactic:
rw [add_comm, aleph0_add_nat]

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
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M₁), f (g (x + y)) = f (g x) + f (g y)

Tactic:
simp only [map_add, forall_const]

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
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M), (⇑f + ⇑g) (x + y) = (⇑f + ⇑g) x + (⇑f + ⇑g) y

Tactic:
by simp [add_comm, add_left_comm]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ ↑h • g • a = g • a

Tactic:
← inv_smul_eq_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ g⁻¹ • ↑h • g • a = a