mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Goal state after:
y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Goal state after:
y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Goal state after:
y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Goal state after:
y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
ext

Goal state after:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ ‖x ^ y‖₊ = ‖x‖₊ ^ y

Tactic:
ext

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ ↑‖x ^ y‖₊ = ↑(‖x‖₊ ^ y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_pos : 0 < p
⊢ 0 < x ^ p

pp: case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p

Tactic:
· exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)

Goal state after:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
· exact (arg_neg_iff.2 hx).le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
⊢ x.toReal ^ z = (x ^ z).toReal

Tactic:
by
  rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (↑m ^ b) r

Tactic:
constructor

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ ↑m ^ b = ↑r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (↑m ^ b) r

Tactic:
constructor

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ ↑m ^ b = ↑r
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
h : f.linear = 0
⊢ f = const k P1 (f (Classical.arbitrary P1))

Tactic:
ext

Goal state after:
case h
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ f p✝ = (const k P1 (f (Classical.arbitrary P1))) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
⊢ (fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f) = f

Tactic:
ext

Goal state after:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p✝ : V1
⊢ ((fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f)) p✝ = f p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₁ →ᵃ[k] P₃
⊢ (fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) x✝) = x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₁ →ᵃ[k] P₃
p✝ : P₁
⊢ ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) x✝)) p✝ = x✝ p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₂ →ᵃ[k] P₄
⊢ (fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) x✝) = x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₂ →ᵃ[k] P₄
p✝ : P₂
⊢ ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) x✝)) p✝ = x✝ p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ (fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f)) = (v, f)

Tactic:
ext

Goal state after:
case fst
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ ((fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).1 = (v, f).1

case snd
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
x✝ : V1
⊢ ((fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).2 x✝ = (v, f).2 x✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x✝¹ x✝ : P₁ →ᵃ[R] V₃
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ + x✝) =
    (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝¹ + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x✝¹ x✝ : P₁ →ᵃ[R] V₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ + x✝)) p✝ =
    ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝¹ + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x✝¹ : R
x✝ : P₁ →ᵃ[R] V₃
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x✝¹ : R
x✝ : P₁ →ᵃ[R] V₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ • x✝)) p✝ =
    ((RingHom.id R) x✝¹ • (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x✝¹ : P₁ →ᵃ[R] P₃
x✝ : P₁ →ᵃ[R] V₃
⊢ (e₁.arrowCongrEquiv e₂) (x✝ +ᵥ x✝¹) = (e₁.arrowCongrₗ e₂.linear) x✝ +ᵥ (e₁.arrowCongrEquiv e₂) x✝¹

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x✝¹ : P₁ →ᵃ[R] P₃
x✝ : P₁ →ᵃ[R] V₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂) (x✝ +ᵥ x✝¹)) p✝ = ((e₁.arrowCongrₗ e₂.linear) x✝ +ᵥ (e₁.arrowCongrEquiv e₂) x✝¹) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
⊢ (pi fun x ↦ 0) = 0

Tactic:
ext

Goal state after:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
p✝ : P1
x✝ : ι
⊢ (pi fun x ↦ 0) p✝ x✝ = 0 p✝ x✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k W)).toFun (x✝¹ + x✝) =
    (e.arrowCongrEquiv (refl k W)).toFun x✝¹ + (e.arrowCongrEquiv (refl k W)).toFun x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k W)).toFun (x✝¹ + x✝)) p✝ =
    ((e.arrowCongrEquiv (refl k W)).toFun x✝¹ + (e.arrowCongrEquiv (refl k W)).toFun x✝) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ : R
x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k W)).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (e.arrowCongrEquiv (refl k W)).toFun x✝

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ : R
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k W)).toFun (x✝¹ • x✝)) p✝ =
    ((RingHom.id R) x✝¹ • (e.arrowCongrEquiv (refl k W)).toFun x✝) p✝
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹) = (congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹

Tactic:
ext

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹)) p✝ = ((congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹) p✝
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]

Tactic:
by
  simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0

case mpr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x = y → x ∈ openSegment 𝕜 x y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]