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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
rw [← prod_filter_ne_one, ← this, prod_biUnion]

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ ∏ x ∈ s, ∏ i ∈ t' x, f i = ∏ x ∈ s, ∏ i ∈ t x, f i

ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ (↑s).PairwiseDisjoint t'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
conv_lhs => rw [Finset.eq_prod_range_div f]
  simp [Finset.prod_range_succ', mul_comm]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (fun n ↦ n • of default) ((lift fun x ↦ 1) x) = x
hy : (fun n ↦ n • of default) ((lift fun x ↦ 1) y) = y
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (x + y)) = x + y

Tactic:
by
      simp only [map_add, add_smul] at *
      rw [hx, hy]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Goal state after:
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 g : S.LocalizationMap N
⊢ f.toMonoidHom = g.toMonoidHom → f = g

Tactic:
by cases f; congr! with eq; ext; exact congr($eq _)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ (f.comp g₁) a = f (g₂ a)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
p r : R
s : ↥S
⊢ p /ₒ s * (r /ₒ 1) = p * r /ₒ s

Tactic:
simp [oreDiv_mul_char p r s 1 p 1 (by simp)]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
a : WithTop α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ StrictMono fun x ↦ a * x

Tactic:
lift a to α using hinf

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
⊢ StrictMono fun x ↦ ↑a * x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
a : WithTop α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
h₀ : 0 < a
hinf : a ≠ ⊤
⊢ StrictMono fun x ↦ x * a

Tactic:
lift a to α using hinf

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
⊢ StrictMono fun x ↦ x * ↑a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
x y : OreLocalization S R
⊢ x * y = y * x

Tactic:
by
    cases x with | _ r₁ s₁
    cases y with | _ r₂ s₂
    rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ : α
ha : ↑a₁ < ↑a₂
b₂ : α
hb : ↑b₁ < ↑b₂
⊢ ↑a₁ * ↑b₁ < ↑a₂ * ↑b₂

Tactic:
norm_cast at *

Goal state after:
case inr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * unbotD 0 ↑a✝

Tactic:
unbotD_coe

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Tactic:
· by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba

Goal state after:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ ¬IsMin a ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
isMin_iff_eq_bot

Goal state after:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ ¬a = ⊥ ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    a
⊢ IsMax a

Tactic:
by
    cases a
    · exact isMax_top
    dsimp only at ha
    split_ifs at ha with ha'
    · exact (not_top_le_coe _ ha).elim
    · rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha
      exact (ha' ha).elim

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
hα : Nonempty α
a✝ : PredOrder (WithTop α)
a : α
h : pred ⊤ = ↑a
c : α
hc : pred ⊤ < ↑c
⊢ False

Tactic:
exact (le_pred_of_lt (coe_lt_top c)).not_gt hc

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ m, n < ↑m

Tactic:
simp_rw [lt_iff_not_ge]
  exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

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

Goal state before:
pp: case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ 1 ≤ c

Tactic:
Order.one_le_iff_ne_zero

Goal state after:
case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ c ≠ 0
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
induction s using Finset.induction generalizing f with
    | empty =>
      obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp
    | insert a s has H => ?_

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : α✝ → β✝
x✝ : Const α α✝
⊢ pure x✝¹ <*> x✝ = x✝¹ <$> x✝

Tactic:
by simp [Const.map, map, Seq.seq, pure, one_mul]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ↑(a ::ₛ ofVector v) = ↑(ofVector (a ::ᵥ v))

Tactic:
cases v
    rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
⊢ IsSuccPrelimit x

Tactic:
by_contra hx

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ False
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt

Goal state after:
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y

Tactic:
exact (hcs₀ hsy).right hysy (h hzsz) hyz

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
⊢ c i ≤ Part.ωSup c

Tactic:
intro x hx
    rw [← eq_some_iff] at hx ⊢
    rw [ωSup_eq_some]
    rw [← hx]
    exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ bot x f
⊢ f y ≤ cSup c

Tactic:
rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'

Goal state after:
case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
· intro h
    have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
    rw [dif_pos h']
    have hh := Classical.choose_spec h'
    rw [eq_of_chain hh h]
    simp

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

Goal state before:
pp: case mk.mk.mk
α✝ β✝ : Type u
a✝ : Cardinal.{u}
α : Type u
b✝ : Cardinal.{u}
β : Type u
c✝ : Cardinal.{u}
γ : Type u
e₁ : α ↪ β
e₂ : β ↪ γ
⊢ Quot.mk (⇑isEquivalent) α ≤ Quot.mk (⇑isEquivalent) γ

Tactic:
exact ⟨e₁.trans e₂⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part (β → γ)
g : α →𝒄 Part β
⊢ (fun x ↦ f x <*> g x) = ⇑(f.bind (flip (_root_.flip map g)))

Tactic:
by
      ext
      simp only [seq_eq_bind_map, Part.bind_eq_bind, Part.mem_bind_iff, flip_apply, _root_.flip,
        map_apply, bind_apply, Part.map_eq_map]

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

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * lift.{u, v} (∏ i, f (some i))

Tactic:
← h fun a => f (some a)

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a ↦ f (some a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀

Tactic:
rcases lt_aleph0.1 ha with ⟨n, rfl⟩

Goal state after:
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ ↑n < ℵ₀

Tactic:
by rw [power_natCast, ← Nat.cast_pow]; apply natCast_lt_aleph0

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

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #↑(⋃ i, f i) ≤ lift.{u, v} #ι * ⨆ i, lift.{v, u} #↑(f i)

Tactic:
refine mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_lift_mk_mul_iSup _)

Goal state after:
α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = sum fun i ↦ lift.{v, u} #↑(f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x : α
⊢ (∃ x y, x ≠ y) ↔ ∃ y, y ≠ x

Tactic:
← nontrivial_iff,

Goal state after:
α : Type u
x : α
⊢ Nontrivial α ↔ ∃ y, y ≠ x
Module: Mathlib.Algebra.Group.Hom.End

Goal state before:
pp: M : Type uM
inst✝ : AddCommGroup M
⊢ instRing.toAddCommGroup.toSubNegMonoid = instRing.toAddGroupWithOne.toAddGroup.toSubNegMonoid

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
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₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ f (g₁ x) = f (g₂ x)

Tactic:
← comp_apply,

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
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₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ (f ∘ₛₗ g₁) x = f (g₂ x)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝² : SetLike S M
inst✝¹ : SMul R M
inst✝ : SMulMemClass S R M
r : R
s : S
⊢ r • ↑s ⊆ ↑s

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝² : SetLike S M
inst✝¹ : SMul R M
inst✝ : SMulMemClass S R M
r : R
s : S
x : M
hx : x ∈ ↑s
⊢ (fun x ↦ r • x) x ∈ ↑s
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
⊢ e (c • a) = c • e a

Tactic:
rw [map_nsmul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -x✝ ∈ s.carrier

Tactic:
← neg_one_mul

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
cases S; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
cases S; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a + x✝ * b) = x✝¹ * (x✝ * (a + b))

Tactic:
← mul_add

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * (a + b)) = x✝¹ * (x✝ * (a + b))
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝¹ : NonUnitalNonAssocSemiring R✝
M : Subsemigroup R✝
R : Type u_1
inst✝ : NonUnitalSemiring R
⊢ (center.instNonUnitalCommSemiring R).toNonUnitalSemiring = NonUnitalSubsemiringClass.toNonUnitalSemiring (center R)

Tactic:
by
  with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalRing R
⊢ (center.instNonUnitalCommRing R).toNonUnitalRing = NonUnitalSubringClass.toNonUnitalRing (center R)

Tactic:
by
  with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝³ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝² : NonAssocSemiring S
inst✝¹ : NonAssocSemiring T
R : Type u_1
inst✝ : Semiring R
⊢ center.commSemiring.toSemiring = (center R).toSemiring

Tactic:
by
  with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ f x ∈ closure (⇑f '' s)

Tactic:
rw [← f.map_closure, Subring.mem_map]

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ x_1 ∈ closure s, f x_1 = f x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
u : Mˣ
hu : (fun x1 x2 ↦ x1 * x2) a b * ↑u = (fun x1 x2 ↦ x1 * x2) a c
⊢ Quot.mk (⇑(Associated.setoid M)) b = Quot.mk (⇑(Associated.setoid M)) c

Tactic:
have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]

Goal state after:
case mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
u : Mˣ
hu✝ : (fun x1 x2 ↦ x1 * x2) a b * ↑u = (fun x1 x2 ↦ x1 * x2) a c
hu : a * (b * ↑u) = a * c
⊢ Quot.mk (⇑(Associated.setoid M)) b = Quot.mk (⇑(Associated.setoid M)) c