mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
induction s using Quotient.inductionOn with | _ l
  simp only [quot_mk_to_coe, mem_coe, coe_erase, noncommProd_coe] at comm h ⊢
  suffices ∀ x ∈ l, ∀ y ∈ l, x * y = y * x by rw [List.prod_erase_of_comm h this]
  intro x hx y hy
  rcases eq_or_ne x y with rfl | hxy
  · rfl
  exact comm hx hy hxy

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

Goal state before:
pp: α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r

Tactic:
exact sInf_le fun _ _ => id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ comap f (r.map f) ≤ r

Tactic:
rw [le_iff_rel_le, comap_rel_eq, coe_map_of_ker_le _ _ hf]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ ((Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) on f) ≤ ⇑r
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
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
    prod_subset (image_subset_iff.2 hest) <| by simpa using h'

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

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
x y : M
⊢ ↑s x y → ↑t x y

Tactic:
hs

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
h :
  { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      s ≤
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
        right_inv := ⋯ }
      t
x y : M
hs : ↑s x y
⊢ ↑t x y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Tactic:
induction m with
  | zero => simp
  | succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi Set.univ P
⊢ Finset.univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ ∈ ⨆ i, map (MonoidHom.mulSingle M i) (P i)

Tactic:
exact noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

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:
← mul_nsmul',

Goal state after:
ι : 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}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
⊢ q ∈ H₂ → ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
hq

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
by
  apply le_antisymm
  · rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
  · rw [prod_le_iff]
    constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f

Tactic:
ext
  rfl

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

Goal state before:
pp: case mk
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b✝ : Localization S
x : M
y : ↥S
⊢ ∃ a, mkHom a = Quot.mk ⇑(OreLocalization.oreEqv S M) (x, y)

Tactic:
exact ⟨⟨x, y⟩, rfl⟩

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 : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j n = k n

Tactic:
exact ((f.map_units s).map j).mul_left_inj.mp <| by rw [← j.map_mul, h, ← k.map_mul, hn, h m]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ IsCancelMul N

Tactic:
simp_rw [isCancelMul_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ ∀ (r : N), IsRightRegular r
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
exact hba.trans (le_succ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : ⟨b, hb⟩ ≤ ⟨c, hc⟩
⊢ ∃ n, pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
simp only [Subtype.mk_le_mk] at hbc

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
⊢ ∃ n, pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩

Tactic:
change dite .. = _

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ (if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩) = ⟨c, hc⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
n : ℕ
hn : pred^[n] c = b
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
induction n generalizing c with

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

Goal state before:
pp: n : ℕ
⊢ n < n + 1

Tactic:
exact lt_add_one n

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 = a

Tactic:
change 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) = a
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 = a

Tactic:
change 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) = a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α 0
⊢ C v

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩

Goal state after:
case zero.nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C ⟨[], ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
v : Vector α 0
w : Vector β 0
⊢ C v w

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩

Goal state after:
case zero.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
w : Vector β 0
⊢ C ⟨[], ⋯⟩ w
Module: Mathlib.Data.Sym.Basic

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

Tactic:
count_replicate

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
v : Vector β 0
w : Vector γ 0
⊢ C ⟨[], ⋯⟩ v w

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩

Goal state after:
case zero.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
w : Vector γ 0
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩ w
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)

pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
· intro b hb
        rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
        exact hb.2 hb.1.2.symm

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ofNat (List α) 0 = []

Tactic:
by rw [← @encode_list_nil α, ofNat_encode]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
by
  refine (List.prod_set v.toList i a).trans ?_
  simp_all

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨hba⟩ | ⟨hba⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ sSup s ∈ s

Tactic:
rwa [← hmin.eq_of_le <| le_csSup hbdd has]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨅ i, f i) = ⨅ i, ⇑(f i)

Tactic:
funext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨆ i, f i) = ⨆ i, ⇑(f i)

Tactic:
funext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b

Tactic:
rw [Part.toOption_eq_none_iff.2 h]

Goal state after:
case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.none.elim b f = b
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ bot x f
s : Set α
⊢ s ∈ {s | IsAdmissible x f s} → cSup c ∈ s

Tactic:
hs

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ bot x f
s : Set α
hs : s ∈ {s | IsAdmissible x f s}
⊢ cSup c ∈ s
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : 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:
rw [Part.toOption_eq_none_iff.2 h]

Goal state after:
case neg
α : 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.none.elim Option.none fun a ↦ (f a).toOption
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ∀ f_1 ∈ {f, g}, ωScottContinuous f_1

Tactic:
rintro f (rfl | rfl | _) <;> assumption

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

Goal state before:
pp: case refine_1
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
intro a b

Goal state after:
case refine_1
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
Module: Mathlib.SetTheory.Cardinal.Order

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

Tactic:
intro a b

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

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))

Tactic:
simp only [ωSup_le_iff]

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ∀ (i : ℕ),
    (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) i ≤
      ωSup
        (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
          (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case top
hm : ⊤ ≠ 0
⊢ ↑⊤ * ℵ₀ = ℵ₀

Tactic:
exact aleph0_mul_aleph0

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = (ψ.comp φ) x

Tactic:
MonoidHom.comp_apply

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = ψ (φ x)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inl
⊢ sInf ∅ = 0

Tactic:
exact Cardinal.sInf_empty

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

Goal state before:
pp: s : Set Cardinal.{u}
⊢ Small.{u, u + 1} ↑s → BddAbove s

Tactic:
by
    rintro ⟨ι, ⟨e⟩⟩
    use sum.{u, u} fun x ↦ e.symm x
    intro a ha
    simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by simp [mul_lt_aleph0_iff, ha, hb]

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
s : R
x y : A
⊢ x * ((algebraMap R A) s * y) = (algebraMap R A) s * (x * y)

Tactic:
left_comm

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ (algebraMap R A) s * (x * y) = (algebraMap R A) s * (x * y)
Module: Mathlib.Algebra.GroupWithZero.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f a✝ : (i : ι) → α i
x✝ : ι
⊢ (a✝ * 0) x✝ = 0 x✝

Tactic:
exact mul_zero _

Goal state after:
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_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ f = g

Tactic:
apply DFunLike.ext

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module S M₃
σ : R →+* S
F : Type u_14
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f g : F
h : ↑f = ↑g
⊢ ∀ (x : M), f x = g x
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✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R M
inst✝³ : Module R N₁
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass R S M
f' : End R M
α : R
hα : α ∈ Set.center R
β : R
x✝ : M
⊢ α • β • x✝ = (RingHom.id R) β • α • x✝

Tactic:
by simp [smul_smul, ((Set.mem_center_iff.mp hα).comm β).eq]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊥ ↔ ¬Nontrivial ↥p

Tactic:
not_nontrivial_iff_subsingleton,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊥ ↔ Subsingleton ↥p
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ ↑e.toIntLinearEquiv = e

Tactic:
ext
  rfl

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

Goal state before:
pp: M : Type u_4
R : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N₁ N₂ : Submodule R M
⊢ Disjoint N₁ N₂ ↔ ∀ {x y : M}, x ∈ N₁ → y ∈ N₂ → x + y = 0 → x = 0 ∧ y = 0

Tactic:
simp only [← Submodule.mem_toAddSubgroup, ← AddSubgroup.disjoint_iff_add_eq_zero]
  aesop (add norm [disjoint_def', AddSubgroup.disjoint_def'])

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ f ∘ₛₗ N.subtype = 0

Tactic:
LinearMap.ext_iff,

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ ∀ (x : ↥N), (f ∘ₛₗ N.subtype) x = 0 x
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * a = ↑n * b
w : n ≠ 0
⊢ a = b

Tactic:
simpa [w] using nat_mul_inj h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 1 ∈ s

Tactic:
by exact hm ▸ sm.one_mem

Goal state after: