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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (q : OreLocalization S X), β q

Tactic:
by
  apply Quotient.ind
  rintro ⟨r, s⟩
  exact c r s

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1

Tactic:
rw [mul_comm, lift_mul_right]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
x : WithZero G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      x =
    x✝ x

Tactic:
cases x

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      0 =
    x✝ 0

case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      ↑a✝ =
    x✝ ↑a✝
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : Injective ⇑(f.lift hg)
x y : M
⊢ g x = g y → f x = f y

Tactic:
intro h

Goal state after:
case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : Injective ⇑(f.lift hg)
x y : M
h : g x = g y
⊢ f x = f y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f ↑(a.2 * b.2) = f (a.1 * ↑b.2)

Tactic:
mul_def,

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f (↑a.2 * ↑b.2) = f (a.1 * ↑b.2)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)

Tactic:
mul_def,

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f (↑a.2 * ↑b.2) = f (↑a.2 * b.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk (x * ↑y) (1 * y) = mk x 1

Tactic:
rhs; rw [← mul_one 1]; rw [← mul_one x]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk (x * 1) (1 * 1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a : M
b : ↥S
⊢ ((monoidOf S).mk' a b).liftOn f H = f a b

Tactic:
rw [← mk_eq_monoidOf_mk', liftOn_mk]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : a✝ * b✝ = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
a b : WithTop α
inst✝ : NoZeroDivisors α
a✝ b✝ : WithTop α
h₁ : (if a✝ = 0 ∨ b✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a✝ b✝) = 0
h₂ : ¬(a✝ = 0 ∨ b✝ = 0)
⊢ False
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
a✝ : α
⊢ x - ↑a✝ ≤ z ↔ x ≤ z + ↑a✝

Tactic:
cases x

Goal state after:
case coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ z ↔ ↑a✝ ≤ z + ↑a✝¹
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
x : OreLocalization S X
⊢ (r /ₒ 1) • x = r • x

Tactic:
cases x

Goal state after:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ (r /ₒ 1) • (r✝ /ₒ s✝) = r • (r✝ /ₒ s✝)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
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
r : R
x : OreLocalization S X
⊢ (r • 1) • x = r • x

Tactic:
cases x

Goal state after:
case c
R : Type u_1
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
r : R
r✝ : X
s✝ : ↥S
⊢ (r • 1) • (r✝ /ₒ s✝) = r • (r✝ /ₒ s✝)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0

Tactic:
cases x

Goal state after:
case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
a✝ : α
⊢ ↑a✝ ^ n = ⊤ ↔ ↑a✝ = ⊤ ∧ n ≠ 0
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y + 1
⊢ x ≤ y

Tactic:
rw [← succ_eq_add_one] at h

Goal state after:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < succ y
⊢ x ≤ y
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n x : ℕ∞
⊢ SuccOrder.succ x = x + 1

Tactic:
cases x

Goal state after:
case top
a b c d m n : ℕ∞
⊢ SuccOrder.succ ⊤ = ⊤ + 1

case coe
a b c d m n : ℕ∞
a✝ : ℕ
⊢ SuccOrder.succ ↑a✝ = ↑a✝ + 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
⊢ ↑⊤.toNat = ⊤ ↔ ⊤ ≠ ⊤

Tactic:
by decide

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

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
⊢ ↑x ≠ ⊤

Tactic:
intro h

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
h : ↑x = ⊤
⊢ False
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
x_top : ↑x ≠ ⊤
⊢ x.inv ≠ ⊤

Tactic:
intro h

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
x_top : ↑x ≠ ⊤
h : x.inv = ⊤
⊢ False
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
coe_pred_of_mem nh

Goal state after:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
nh : pred ↑a ∈ s
h : pred ↑a = ↑a
⊢ False
Module: Mathlib.Data.ENat.Basic

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

Tactic:
by
  simp [← map_natCast_inj (α := α)]

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

Goal state before:
pp: n : ℕ
m : WithBot ℕ∞
⊢ ↑n + 1 ≤ m ↔ ↑n < m

Tactic:
by
  rw [← WithBot.coe_one, ← natCast_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
  cases m
  · simp
  · rw [WithBot.coe_le_coe, natCast_add, natCast_one, ENat.add_one_le_iff (natCast_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]

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

Goal state before:
pp: a b : WithBot ℕ∞
c : ℕ
⊢ ↑c + a ≤ ↑c + b ↔ a ≤ b

Tactic:
by
  rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
rw [Finset.prod_eq_one]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ ∀ x ∈ s, (if h : a = x then b x h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1

Tactic:
rw [Finset.prod_eq_one]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ ∀ x ∈ s, (if h : x = a then b x h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∀ i ∈ s, ¬p i
⊢ ∀ x ∈ s, (if p x then a else 1) = 1

Tactic:
exact fun i hi => if_neg (h i hi)

Goal state after:
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 => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ a ::ᵥ v.tail = a ::ᵥ v'

Tactic:
h.2

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ a ::ᵥ v' = a ::ᵥ v'
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 → 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)
u : Vector α 0
v : Vector β 0
w : Vector γ 0
⊢ C u v w

Tactic:
rcases u 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 → 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
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Tactic:
· refine congr_arg Sum.inr ?_
      refine map_injective (Option.some_injective _) _ ?_
      refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_) <;> simp

Goal state after:
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(Set.range Subtype.val ∪ t)

Tactic:
← Subtype.range_val (s := t),

Goal state after:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(Set.range Subtype.val ∪ Set.range Subtype.val)
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 : ℕ
α✝ : Type u
x : flip Vector n α✝
⊢ id <$> x = x

Tactic:
cases x

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : val✝.length = n
⊢ id <$> ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
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 : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x : flip Vector n α✝
⊢ (h✝ ∘ g✝) <$> x = h✝ <$> g✝ <$> x

Tactic:
cases x

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : val✝.length = n
⊢ (h✝ ∘ g✝) <$> ⟨val✝, property✝⟩ = h✝ <$> g✝ <$> ⟨val✝, property✝⟩
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ (¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b) → Surjective ⇑f

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
⊢ Surjective ⇑f
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 : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (⋯.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}
        ⋯)

Tactic:
exact WellFounded.not_lt_min _ {b | ∀ a', r a' a → s (collapseF f a') b} h

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a → ∃ c ≤ a, f c = b

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b ≤ f a
⊢ ∃ c ≤ a, f c = b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a → ∃ a' < a, f a' = b

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b < f a
⊢ ∃ a' < a, f a' = b
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case mp
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂

Tactic:
intro h

Goal state after:
case mp
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
⊢ ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
intro h

Goal state after:
case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
      intro n
      induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]

Goal state after:
case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
intro h

Goal state after:
α : Type u_1
x : α
h : some x = none
⊢ False
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o.toOption ↔ a ∈ o

Tactic:
mem_toOption

Goal state after:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o ↔ a ∈ o
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y

Tactic:
intro h

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y
Module: Mathlib.Data.Part

Goal state before:
pp: case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y

Tactic:
intro h

Goal state after:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
H : ∃ m, Maximal (fun x_1 ↦ x_1 ∈ {y | y ∈ s ∧ x ≤ y}) m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m

Tactic:
rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
m : α
hm : ∀ ⦃y : α⦄, (fun x_1 ↦ x_1 ∈ {y | y ∈ s ∧ x ≤ y}) y → m ≤ y → y ≤ m
hms : m ∈ s
hxm : x ≤ m
⊢ ∃ m, x ≤ m ∧ Maximal (fun x ↦ x ∈ s) m
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

Goal state after:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ Quot.mk (⇑isEquivalent) α ≤ Quot.mk (⇑isEquivalent) α

Tactic:
exact ⟨Embedding.refl _⟩

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ sum f

Tactic:
← Quotient.out_eq (f i)

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ↑(toNat a) ≤ a

Tactic:
obtain h | h := lt_or_ge a ℵ₀

Goal state after:
case inl
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ ↑(toNat a) ≤ a

case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
h : Fintype α✝
α β : Type u
⊢ ∀ [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
hβ

Goal state after:
case refine_1
α✝ : Type u
h : Fintype α✝
α β : Type u
hβ : Fintype β
⊢ ∀ (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ ¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}

Tactic:
intro h

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · by_cases ha : a = 0
    · exact Or.inl ha
    right
    by_cases hb : b = 0
    · exact Or.inl hb
    right
    rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb
    constructor
    · rw [← mul_one a]
      exact (mul_le_mul' le_rfl hb).trans_lt h
    · rw [← one_mul b]
      exact (mul_le_mul' ha le_rfl).trans_lt h
  rintro (rfl | rfl | ⟨ha, hb⟩) <;> simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

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

Goal state before:
pp: α β : Type u
s : Set α
t : Set β
⊢ #↑(s ×ˢ t) = #↑s * #↑t

Tactic:
mul_def,

Goal state after:
α β : Type u
s : Set α
t : Set β
⊢ #↑(s ×ˢ t) = #(↑s × ↑t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
s : Set α
n : ℕ
h : #↑s = ↑n
⊢ ∃ t, ↑t = s ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
have : ↑(3 : ℕ) ≤ #α := by simpa using h

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ∃ z, z ≠ x ∧ z ≠ y
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst✝⁵ : SMul A B
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Algebra B C
inst✝¹ : SMul A C
inst✝ : IsScalarTower A B C
⊢ ↑(a • b) = a • ↑b

Tactic:
by
  simp [Algebra.algebraMap_eq_smul_one]

Goal state after: