mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
·

Goal state after:
case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
·

Goal state after:
case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : x ≠ 0
⊢ Monotone fun y ↦ x ^ y

Tactic:
intro y z y_z

Goal state after:
x : ℕ∞
h : x ≠ 0
y z : ℕ∞
y_z : y ≤ z
⊢ (fun y ↦ x ^ y) y ≤ (fun y ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
⊢ (fun y ↦ x ^ y) ⊤ ≤ (fun y ↦ x ^ y) z

pp: case coe
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a✝ : ℕ
y_z : ↑a✝ ≤ z
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) z

Tactic:
·

Goal state after:
case top
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
⊢ (fun y ↦ x ^ y) ⊤ ≤ (fun y ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

pp: case coe.coe
x : ℕ∞
h : x ≠ 0
a✝¹ a✝ : ℕ
y_z : ↑a✝¹ ≤ ↑a✝
⊢ (fun y ↦ x ^ y) ↑a✝¹ ≤ (fun y ↦ x ^ y) ↑a✝

Tactic:
·

Goal state after:
case coe.top
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top.inl
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_0 : x < 1
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

pp: case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

pp: case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
·

Goal state after:
case coe.top.inl
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_0 : x < 1
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

pp: case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
·

Goal state after:
case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
·

Goal state after:
case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe.coe
x : ℕ∞
h : x ≠ 0
a✝¹ a✝ : ℕ
y_z : ↑a✝¹ ≤ ↑a✝
⊢ (fun y ↦ x ^ y) ↑a✝¹ ≤ (fun y ↦ x ^ y) ↑a✝

Tactic:
·

Goal state after:
case coe.coe
x : ℕ∞
h : x ≠ 0
a✝¹ a✝ : ℕ
y_z : ↑a✝¹ ≤ ↑a✝
⊢ (fun y ↦ x ^ y) ↑a✝¹ ≤ (fun y ↦ x ^ y) ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ ⊤ ≤ z ^ ⊤

pp: case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝

Tactic:
·

Goal state after:
case top
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ ⊤ ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ x ^ ⊤ ≤ z ^ ⊤

pp: case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ^ ⊤ ≤ z ^ ⊤

pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
·

Goal state after:
case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ x ^ ⊤ ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ^ ⊤ ≤ z ^ ⊤

pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ^ ⊤ ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∑ i ∈ f.support ∪ g.support, f i • v i = ∑ i ∈ f.support ∪ g.support, g i • v i

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ x✝ ∈ f.support ∪ g.support

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∑ i ∈ f.support ∪ g.support, f i • v i = ∑ i ∈ f.support ∪ g.support, g i • v i
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝

Tactic:
·

Goal state after:
case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_1
x y : ℕ∞
h : x ^ y = 0
⊢ x = 0

pp: case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False

Tactic:
·

Goal state after:
case refine_1
x y : ℕ∞
h : x ^ y = 0
⊢ x = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False

Tactic:
·

Goal state after:
case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

pp: case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1

pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
·

Goal state after:
case inl
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1

pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
·

Goal state after:
case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
·

Goal state after:
case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y z : ℕ∞
x_0 : x < 1
⊢ x ^ (y + z) = x ^ y * x ^ z

pp: case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
·

Goal state after:
case inl
x y z : ℕ∞
x_0 : x < 1
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl.inl
x z : ℕ∞
x_0 : x < 1
⊢ 0 ^ (0 + z) = 0 ^ 0 * 0 ^ z

pp: case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
·

Goal state after:
case inl.inl
x z : ℕ∞
x_0 : x < 1
⊢ 0 ^ (0 + z) = 0 ^ 0 * 0 ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
·

Goal state after:
case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
·

Goal state after:
case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ x✝ ∈ f.support ∪ g.support

Tactic:
·

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ x✝ ∈ f.support ∪ g.support
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
·

Goal state after:
case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∪ g.support
⊢ f x✝ = g x✝

Tactic:
notMem_union,

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∧ x✝ ∉ g.support
⊢ f x✝ = g x✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = x ^ ⊤ * x ^ z

pp: case inr.inr.coe
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + z) = x ^ ↑a✝ * x ^ z

Tactic:
·

Goal state after:
case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = x ^ ⊤ * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + ⊤) = x ^ ↑a✝ * x ^ ⊤

pp: case inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ a✝ : ℕ
⊢ x ^ (↑a✝¹ + ↑a✝) = x ^ ↑a✝¹ * x ^ ↑a✝

Tactic:
·

Goal state after:
case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + ⊤) = x ^ ↑a✝ * x ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

pp: case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝

Tactic:
·

Goal state after:
case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
x y z : ℕ∞
x_0 : x < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

pp: case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤

pp: case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inl
x y z : ℕ∞
x_0 : x < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤

pp: case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inl
x y z : ℕ∞
x_2 : 1 < x
y_0 : y < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

pp: case top.inr.inr.inr.inl
x z : ℕ∞
x_2 : 1 < x
⊢ (x * 1) ^ ⊤ = x ^ ⊤ * 1 ^ ⊤

pp: case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inr.inl
x y z : ℕ∞
x_2 : 1 < x
y_0 : y < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inr.inl
x z : ℕ∞
x_2 : 1 < x
⊢ (x * 1) ^ ⊤ = x ^ ⊤ * 1 ^ ⊤

pp: case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inr.inr.inl
x z : ℕ∞
x_2 : 1 < x
⊢ (x * 1) ^ ⊤ = x ^ ⊤ * 1 ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
·

Goal state after:
case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝

Tactic:
·

Goal state after:
case coe
x y z : ℕ∞
a✝ : ℕ
⊢ (x * y) ^ ↑a✝ = x ^ ↑a✝ * y ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y z : ℕ∞
y_0 : y = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

pp: case inr
x y z : ℕ∞
y_0 : y ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
·

Goal state after:
case inl
x y z : ℕ∞
y_0 : y = 0
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

pp: case inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
·

Goal state after:
case inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z = 0
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ x ^ (y * z) = (x ^ y) ^ z

pp: case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z

pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
·

Goal state after:
case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z

pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
·

Goal state after:
case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
·

Goal state after:
case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ x ^ (⊤ * z) = (x ^ ⊤) ^ z

pp: case inr.inr.inr.inr.coe
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝ * z) = (x ^ ↑a✝) ^ z

Tactic:
·

Goal state after:
case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ x ^ (⊤ * z) = (x ^ ⊤) ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ (↑a✝ * ⊤) = (x ^ ↑a✝) ^ ⊤

pp: case inr.inr.inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ : ℕ
y_0 : ↑a✝¹ ≠ 0
a✝ : ℕ
z_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝¹ * ↑a✝) = (x ^ ↑a✝¹) ^ ↑a✝

Tactic:
·

Goal state after:
case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ (↑a✝ * ⊤) = (x ^ ↑a✝) ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ : ℕ
y_0 : ↑a✝¹ ≠ 0
a✝ : ℕ
z_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝¹ * ↑a✝) = (x ^ ↑a✝¹) ^ ↑a✝

Tactic:
·

Goal state after:
case inr.inr.inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ : ℕ
y_0 : ↑a✝¹ ≠ 0
a✝ : ℕ
z_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝¹ * ↑a✝) = (x ^ ↑a✝¹) ^ ↑a✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i) →
    ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) →
    ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i

Tactic:
·

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i) →
    ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) →
    ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i

Tactic:
·

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) →
    ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x, f (finSumFinEquiv.toFun x) = (∏ i, f (castAdd b i)) * ∏ i, f (natAdd a i)

pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
·

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x, f (finSumFinEquiv.toFun x) = (∏ i, f (castAdd b i)) * ∏ i, f (natAdd a i)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
·

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y

pp: case refine_1
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ x) = (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ y)

Tactic:
·

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m n, m • p + a = n • p + b) → ∃ m, m • p = b - a

pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m, m • p = b - a) → ∃ m n, m • p + a = n • p + b

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m n, m • p + a = n • p + b) → ∃ m, m • p = b - a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m, m • p = b - a) → ∃ m n, m • p + a = n • p + b

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m, m • p = b - a) → ∃ m n, m • p + a = n • p + b
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) → ∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p

pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p) → ∃ m, a - b = m • p

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) → ∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n

pp: case mp.refine_2
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ a - b = (k / ↑n * ↑n + k % ↑n) • p

Tactic:
·

Goal state after:
case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n