mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

Tactic:
cases a <;> simp

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

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

Tactic:
lift b₁ to α using hb.lt_top.ne

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

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊥ * ⊥ = if ⊥ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ⊥

Tactic:
aesop

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

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊥ * ↑a✝ = if ⊥ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ↑a✝

Tactic:
aesop

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

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊥ = if ↑a✝ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊥

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b) = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ y - 1 = x

Tactic:
rw [← pred_eq_sub_one]
  exact pred_eq_iff_covBy.symm

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

Goal state before:
pp: case coe.top
a : ℕ
⊢ (↑a * ⊤).toNat = (↑a).toNat * ⊤.toNat

Tactic:
cases a <;> simp

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(pred a) = pred ↑a

Tactic:
change Subtype.val (dite ..) = _

Goal state after:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(if h : pred ↑a ∈ s then ⟨pred ↑a, h⟩ else a) = pred ↑a
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ 0 ≤ map Nat.cast n

Tactic:
by cases n <;> simp

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(succ a) = succ ↑a

Tactic:
change Subtype.val (dite ..) = _

Goal state after:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = succ ↑a
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)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (s.piecewise f g i)

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (s.piecewise f g i)

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∉ s
⊢ p (s.piecewise f g i)
Module: Mathlib.Data.Fintype.Sigma

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
aesop

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

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

Tactic:
aesop

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ a ∈ univ, ↑a ∈ s

Tactic:
aesop

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

Goal state before:
pp: case refine_3
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

Tactic:
aesop

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

Goal state before:
pp: case refine_4
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ a ∈ univ, ⟨↑a, ⋯⟩ = a

Tactic:
aesop

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

Goal state before:
pp: case refine_5
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = g ↑⟨a, ha⟩ ⋯

Tactic:
aesop

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

Goal state before:
pp: case neg.h
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ s = s \ {i}

Tactic:
aesop

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

Goal state before:
pp: case neg.a
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ ∀ x ∈ s \ {i}, f x = f x

Tactic:
aesop

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

Goal state before:
pp: case h.inr.a
α : 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)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a

Tactic:
· exact g'.injective.ne (ne_of_mem_of_not_mem hi has)

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

Goal state before:
pp: β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i, c i = ∏ i, if h : ↑i < n then c ⟨↑i, h⟩ else 1

Tactic:
Finset.prod_congr rfl

Goal state after:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ univ.prod ?m.36 = ∏ i, if h : ↑i < n then c ⟨↑i, h⟩ else 1

β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ x ∈ univ, c x = ?m.36 x

β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ Fin n → β
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ β₁}, ((↑ea).sumCongr ↑eb) a ≤ ((↑ea).sumCongr ↑eb) b ↔ a ≤ b

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
⊢ IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
ht : IsLowerSet t
⊢ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ⋯.min
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s (↑(IsWellFounded.fix r (fun a IH ↦ ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1))
              b}
      ⋯ ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s (↑(IsWellFounded.fix r (fun a IH ↦ ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩) a')) b}

Tactic:
exact WellFounded.min_mem _ _ _

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f.top = g.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
let f := f.subrelIso
        rw [h] at f
        exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩

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✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
a b : α
hab : a ≤ b
x✝² x✝¹ : ℕ
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝² ≤
    (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝¹

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ ((pair a b hab) 0 = x✝ ∨ ∃ n, (pair a b hab) (n + 1) = x✝) ↔ x✝ ∈ {a, b}

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y / x) b).get ⋯ = a.get ⋯ / b.get ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 % a = ma % mb

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f = ⨆ n, (⇑f)^[n] ⊥

Tactic:
by
  apply le_antisymm
  · apply lfp_le_fixed
    exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)
  · apply le_lfp
    intro a h_a
    exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y % x) b).get ⋯ = a.get ⋯ % b.get ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ++ a = ma ++ mb

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯

Tactic:
aesop

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
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb

Tactic:
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.bind fun y ↦ map (fun x ↦ y ∩ x) b).get ⋯ = a.get ⋯ ∩ b.get ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∪ a = ma ∪ mb

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ∪ x) b).get ⋯ = a.get ⋯ ∪ b.get ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 \ a = ma \ mb

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

Tactic:
rw [forall_comm, forall_forall_merge]

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:
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.ENat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a = ↑(toENat a) ↔ a ≤ ℵ₀

Tactic:
← enat_gc.exists_eq_l

Goal state after:
a : Cardinal.{u_1}
⊢ (∃ b, a = ↑b) ↔ a ≤ ℵ₀
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case inr.inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 0
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

Tactic:
simp [Int.sign_eq_zero_iff_zero.mp h]

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ c < ↑n + 1 ↔ c ≤ ↑n

Tactic:
by
  rw [← Order.lt_succ_iff, succ_natCast]

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ Nonempty (α ≃ Fin n)

Tactic:
by
  rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']

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

Goal state before:
pp: R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • r • 1 = r • 1

Tactic:
smul_comm a r (1 : A),

Goal state after:
R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ r • a • 1 = r • 1
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Module S M₂
σ : R →+* S
f g : M →ₑ+[↑σ] M₂
h : ↑f = ↑g
⊢ f = g

Tactic:
by
  ext m
  exact LinearMap.congr_fun h m

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M
inst✝ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
f : M →ₛₗ[σ₁₂] M₂
⊢ ⇑f = 0 ↔ f = 0

Tactic:
aesop

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

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x✝ : X
⊢ ((f.inverse' g k₂ h₁ h₂).comp f) x✝ = (MulActionHom.id M) x✝

Tactic:
simpa using h₁.eq _

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

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f (x • 1) = g (x • 1)

Tactic:
f.map_smulₑ,

Goal state after:
R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ σ x • f 1 = g (x • 1)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b : A
h : mulLeft R a = mulLeft R b
⊢ a = b

Tactic:
simpa using LinearMap.ext_iff.mp h 1

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : A
h : mulRight R a = mulRight R b
⊢ a = b

Tactic:
simpa using LinearMap.ext_iff.mp h 1

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
m m' : M
⊢ f.smulRight (m + m') = f.smulRight m + f.smulRight m'

Tactic:
by
        ext
        apply smul_add

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (m : PUnit), 0 • m = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (b : PUnit), 1 • b = b

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R), r • 1 = 1

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (x : PUnit), 0 • x = 0

Tactic:
by subsingleton

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∪ ↑t → c • x ∈ ↑s ∪ ↑t

Tactic:
aesop

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∩ ↑t → c • x ∈ ↑s ∩ ↑t

Tactic:
aesop

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

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋃ s ∈ S, ↑s → c • x ∈ ⋃ s ∈ S, ↑s

Tactic:
aesop

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

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
⊢ map (f + g) p ≤ map f p ⊔ map g p

Tactic:
by
  rintro x ⟨m, hm, rfl⟩
  exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ ↑((equivMapOfInjective f i p).symm ((equivMapOfInjective f i p) ((equivMapOfInjective f i p).symm x))) =
    ↑((equivMapOfInjective f i p).symm x)

Tactic:
LinearEquiv.apply_symm_apply

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ ↑((equivMapOfInjective f i p).symm x) = ↑((equivMapOfInjective f i p).symm x)