mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y

Tactic:
cases y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
y : OreLocalization S X
r₁ : M
s₁ : ↥S
⊢ r • (r₁ /ₒ s₁) • y = (r₁ /ₒ s₁) • r • y

Tactic:
cases y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r • (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ /ₒ s₁) • r • (r₂ /ₒ s₂)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
exact h₀

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
ihn : 0 < 0 → (∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)) → x 0 < y 0
hn : 0 < 0 + 1
hx : ∀ (k : ℕ), k < 0 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 + 1 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
exact h₀

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

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)

Tactic:
cases y with | _ r₂ s₂

Goal state after:
case c.c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₂ /ₒ s₂ * (r₁ /ₒ s₁)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₁) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) n₁ n₂

Tactic:
a

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) a n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₁) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) n₁ n₂

Tactic:
a

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) a n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₁) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂

Tactic:
a

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) a n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₁) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂

Tactic:
a

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) a n₂
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a✝ : αᵒᵈ
h : a✝ ≤ (⇑toDual ∘ SuccOrder.succ ∘ ⇑ofDual) a✝
⊢ IsMin a✝

Tactic:
by apply SuccOrder.max_of_succ_le h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

Tactic:
apply lt_of_le_of_ne h (ne_of_not_le nh).symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ a < b

Tactic:
le_iff_eq_or_lt

Goal state after:
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a = b ∨ a < b ↔ a = b ∨ a < b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
⊢ a ≤ b ↔ ∀ c < a, c ≤ b

Tactic:
use fun ha c hc ↦ hc.le.trans ha
  intro H
  by_contra! ha
  exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_gt hb⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a < succ b

Tactic:
le_iff_eq_or_lt

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a = succ b ∨ a < succ b ↔ a = succ b ∨ a < succ b
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ x + 1

Tactic:
by
  rw [← succ_eq_add_one]
  exact covBy_succ x

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

Goal state before:
pp: α : 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
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b

Tactic:
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le

Goal state after:
α : 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 : ℕ
ha : pred^[n] b ∈ s
hab : pred^[n] b < b
⊢ f (pred^[n] b) < f b
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 ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if a = x then b x else 1) = b a

Tactic:
by
  simp only [prod_ite_eq, if_pos h]

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:
by
  rw [prod_eq_mul_prod_sdiff_singleton_of_mem h, mul_comm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
Finset.prod_eq_mul_prod_sdiff_singleton_of_mem ha

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr
α : 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'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
Equiv.trans_apply,

Goal state after:
case h.inr
α : 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
⊢ ↑((Equiv.swap ⟨f a, hfat⟩ (g' a)) (g' i)) = f i
Module: Mathlib.Data.Fintype.Sum

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

Tactic:
have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using! hfst

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β

Tactic:
contrapose! H

Goal state after:
α : Type u_1
β : Type u_2
H : Finite α ∧ Finite β
⊢ Finite (α ⊕ β)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ ∀ (x : α), x ∈ v.toList → p x

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
        exact hp.2

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

Goal state before:
pp: case succ
α : 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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (n + 1)
v : Vector β (n + 1)
w : Vector γ (n + 1)
⊢ C u v w

Tactic:
rcases u with ⟨_ | ⟨a, u⟩, u_property⟩

Goal state after:
case succ.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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
u_property : [].length = n + 1
⊢ C ⟨[], u_property⟩ v w

case succ.cons
α : 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)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
⊢ C ⟨a :: u, u_property⟩ v w
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ⟨((↑v).insertIdx j a).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ =
    ⟨(↑(match v with
            | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
        (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a,
      ⋯⟩

Tactic:
Subtype.mk_eq_mk

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ((↑v).insertIdx j a).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #(image List.ofFn univ) = Fintype.card α ^ s

Tactic:
simp [card_image_of_injective univ List.ofFn_injective]

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
rintro ⟨S, hSc, hps, hS⟩
    rcases eq_empty_or_nonempty S with (rfl | hne)
    · rw [sSup_empty] at hS
      have := subsingleton_of_bot_eq_top hS
      rcases h with ⟨x, hx⟩
      exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
    · rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
      refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
      rwa [hs.iSup_comp, ← sSup_eq_iSup']

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α⦄, IsLUB d a → IsLUB (g ∘ f '' d) ((g ∘ f) a)

Tactic:
a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
⊢ IsLUB d a → IsLUB (g ∘ f '' d) ((g ∘ f) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a✝ : α
hb : a✝ ∈ d
⊢ f a✝ ≤ p₁

Tactic:
exact (hp _ hb).1

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α × β⦄, IsLUB d a → IsLUB (Prod.fst '' d) a.1

Tactic:
a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
⊢ IsLUB d a → IsLUB (Prod.fst '' d) a.1
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α × β⦄, IsLUB d a → IsLUB (Prod.snd '' d) a.2

Tactic:
a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
⊢ IsLUB d a → IsLUB (Prod.snd '' d) a.2
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x

Tactic:
exact h₀

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)

Tactic:
simp [mul_def]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)

Tactic:
by simp [union_def]

Goal state after:
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.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
intro c hc
    refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩
    intro y hy hy'
    obtain ⟨z, hz, hzy⟩ : ∃ z ∈ c, ¬ (f z ≤ y) := by
      by_contra! h
      apply lt_irrefl y (lt_of_lt_of_le hy' ?_)
      apply cSup_le
      intro z hz
      exact le_trans (le_map z) (h z hz)
    have h : y ≤ z := by
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy
      exact Or.resolve_right hy.2 hzy
    obtain hyz | rfl := le_iff_lt_or_eq.1 h
    · exact le_trans ((hc hz).map_le_of_mem_of_lt hy hyz) (le_cSup _ _ hz)
    · have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'
      apply hc'.2.resolve_left
      intro hc'
      exact lt_irrefl y (lt_of_lt_of_le hy' hc')

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:
forall_comm,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (b a : ℕ), (c₀ b) (c₁ a) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
hα : Quot.mk (⇑isEquivalent) α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α ^ Quot.mk (⇑isEquivalent) γ

Tactic:
exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

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

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

Tactic:
wlog hle : x ≤ y; · rw [add_comm, this y x (le_of_not_ge hle), add_comm]
    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.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
a : R
inst✝¹ : SMul R M
inst✝ : SMul S M
f : R → S
smul : ∀ (m : M), f a • m = a • m
⊢ IsSMulRegular M (f a) ↔ IsSMulRegular M a

Tactic:
by simp [IsSMulRegular, smul]

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

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = lift.{u, v} 1

Tactic:
lift_one,

Goal state after:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • m₂ - r • m₂ = 0

Tactic:
sub_self

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

Goal state before:
pp: α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
⊢ #α ≤ ↑n

Tactic:
contrapose! H

Goal state after:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ∃ s, n < s.card
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✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Surjective (⇑g ∘ ⇑f)

Tactic:
simp_rw [← coe_comp, h, id_coe, bijective_id.2]

Goal state after: