mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
⊢ |(-↑π).toReal| = |(↑π).toReal|

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ = ↑(π / 2) ∨ θ.toReal = -π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
toReal_eq_neg_pi_div_two_iff

Goal state after:
θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = ↑(-π / 2) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Tactic.Rify

Goal state before:
pp: a b : ℚ
⊢ a = b ↔ ↑a = ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Rify

Goal state before:
pp: a b : ℚ
⊢ a ≤ b ↔ ↑a ≤ ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Rify

Goal state before:
pp: a b : ℚ
⊢ a < b ↔ ↑a < ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Rify

Goal state before:
pp: a b : ℚ
⊢ a ≠ b ↔ ↑a ≠ ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
arg_mul_cos_add_sin_mul_I_eq_toIocMod hr,

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.zero
x : ℂ
x0 : x ≠ 0
⊢ ↑(x ^ 0).arg = 0 • ↑x.arg

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
⊢ (↑π).toReal ∈ Set.Ioo 0 π ↔ (↑π).sign = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg ∘ Neg.neg) x

Tactic:
←
      Function.comp_assoc

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x

Tactic:
refine ContinuousAt.comp ?_ continuous_neg.continuousAt

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ 0 < x ^ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 0) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 1) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 1 * 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹

Tactic:
split_ifs <;> simp_all [exp_neg]

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

Goal state before:
pp: a : ℝ
ha : a ≤ 1
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y).re / rexp (x.arg * (↑y).im) = ‖x‖ ^ y

Tactic:
simp

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

Goal state before:
pp: x : ℂ
y : ℝ
⊢ x = 0 → (↑y).re = 0 → ↑y = 0

Tactic:
simp

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ x ^ 2 = x ^ 2

Tactic:
simp

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

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

Tactic:
Real.rpow_def_of_nonneg

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z

pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
Real.rpow_def_of_nonneg

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rw [← rpow_natCast, ← rpow_mul hx, mul_inv_cancel₀ hn0, rpow_one]

Goal state after:
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:
by
  ext; exact Real.rpow_add_natCast (mod_cast hx) _ _

Goal state after:
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:
exact Real.rpow_sub_natCast' (mod_cast x.2) h

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

Goal state before:
pp: case inr.inl
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

Tactic:
simp

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

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ 1 = x

Tactic:
simp

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

Goal state before:
pp: case inr.inl
y z : ℝ
hx₀ : 1 ≠ 0
⊢ 1 ^ y = 1 ^ z ↔ y = z ∨ 1 = 1 ∨ 1 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

Tactic:
simp

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

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

Tactic:
simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]

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

Goal state before:
pp: x : ℝ
⊢ ↑(1 ^ x) = ↑1

Tactic:
simp

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

Goal state before:
pp: x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : y < 1
⊢ x < x ^ y

Tactic:
by
  simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

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

Goal state before:
pp: x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : 1 < y
⊢ x ^ y < x

Tactic:
by
  simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

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

Goal state before:
pp: case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ 0 < 0 then ∞ else x ^ 0 * y ^ 0

Tactic:
simp

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

Goal state before:
pp: x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
⊢ x ≤ y ^ z

Tactic:
obtain hx | hx := le_or_gt x 0
  · exact hx.trans (rpow_pos_of_pos hy _).le
  · exact (le_rpow_iff_log_le hx hy).2 h

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ ∅, ↑(f i) ^ r = ↑(∏ i ∈ ∅, f i) ^ r

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hf : ∀ i ∈ ∅, f i ≠ ∞
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
simp

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

Goal state before:
pp: hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) a✝¹ ≤ (fun x ↦ 1 ^ x) b✝

Tactic:
simp

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

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝¹

Tactic:
simp

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

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)

Tactic:
simp

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

Goal state before:
pp: case h₁
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ a ≤ max a b

Tactic:
simp

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

Goal state before:
pp: case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ b ≤ max a b

Tactic:
simp

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

Goal state before:
pp: case h₂.ha
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ a ^ p

Tactic:
simp

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

Goal state before:
pp: case hb
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ b ^ p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ 0 -ᵥ x = y -ᵥ (x + y)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x x +ᵥ midpoint R (-y) y = x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y : M
x : Ray R M
⊢ ∀ (v : M) (hv : v ≠ 0), - -rayOfNeZero R v hv = rayOfNeZero R v hv

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ (map f) (-rayOfNeZero R g hg) = -(map f) (rayOfNeZero R g hg)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: 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 g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : f p = g p
q : P1
⊢ g.linear (q -ᵥ p) = g.toFun ((q -ᵥ p) +ᵥ q) -ᵥ g.toFun q

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
p : P2
x✝¹ : P1
x✝ : V1
this : AddAction V2 P2 := inferInstance
⊢ Function.const P1 p (x✝ +ᵥ x✝¹) = 0 x✝ +ᵥ Function.const P1 p x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
g : P1 →ᵃ[k] P3
⊢ ∀ (p : P1) (v : V1), Function.prod (⇑f) (⇑g) (v +ᵥ p) = (f.linear.prod g.linear) v +ᵥ Function.prod (⇑f) (⇑g) p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] P2
g : P3 →ᵃ[k] P4
⊢ ∀ (p : P1 × P3) (v : V1 × V3), Prod.map (⇑f) (⇑g) (v +ᵥ p) = (f.linear.prodMap g.linear) v +ᵥ Prod.map (⇑f) (⇑g) p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ lineMap p₀ p₁ = (lineMap p₁ p₀).comp (lineMap 1 0)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₁ P₁
inst✝ : AffineSpace V₂ P₂
e e' : P₁ ≃ᵃ[k] P₂
⊢ ⇑e = ⇑e' ↔ e = e'

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₁ P₁
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ range ⇑e = univ

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₁ P₁
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
p₁ p₂ : P₁
⊢ e p₁ = e p₂ ↔ p₁ = p₂

Tactic:
simp

Goal state after:
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₄
⊢ ∀ (p : P₁ × P₃) (v : V₁ × V₃),
    ((↑e₁).prodCongr ↑e₂) (v +ᵥ p) = (e₁.linear.prodCongr e₂.linear) v +ᵥ ((↑e₁).prodCongr ↑e₂) p

Tactic:
simp

Goal state after:
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₄
⊢ ∀ (p : P₁ × P₂) (v : V₁ × V₂),
    (Equiv.prodComm P₁ P₂) (v +ᵥ p) = (LinearEquiv.prodComm k V₁ V₂) v +ᵥ (Equiv.prodComm P₁ P₂) p

Tactic:
simp

Goal state after:
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₄
⊢ ∀ (p : (P₁ × P₂) × P₃) (v : (V₁ × V₂) × V₃),
    (Equiv.prodAssoc P₁ P₂ P₃) (v +ᵥ p) = (LinearEquiv.prodAssoc k V₁ V₂ V₃) v +ᵥ (Equiv.prodAssoc P₁ P₂ P₃) p

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
x y : E
⊢ [x -[R] y] ⊆ [x -[𝕜] y]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hxy⟩
  refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
  all_goals exact zero_smul R (1 : 𝕜) ▸ smul_le_smul_of_nonneg_right ‹_› zero_le_one

Goal state after:
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
⊢ ∀ (x y : V1 →ᵃ[k] V2), ((x + y) 0, (x + y).linear) = (x 0, x.linear) + (y 0, y.linear)

Tactic:
simp

Goal state after:
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
⊢ ∀ (m : R) (x : V1 →ᵃ[k] V2), ((m • x) 0, (m • x).linear) = (RingHom.id R) m • (x 0, x.linear)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ x : P
⊢ ((ofLinearEquiv A p₀ p₁).trans (ofLinearEquiv B p₁ p₂)) x = (ofLinearEquiv (A ≪≫ₗ B) p₀ p₂) x

Tactic:
simp

Goal state after:
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
p✝ : V1
⊢ ((fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f)) p✝ = (⇑f.linear + fun x ↦ f 0) p✝

Tactic:
simp

Goal state after:
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₃
p✝ : P₁
⊢ ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) x✝)) p✝ = x✝ p✝

Tactic:
simp

Goal state after:
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₄
p✝ : P₂
⊢ ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) x✝)) p✝ = x✝ p✝

Tactic:
simp

Goal state after:
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₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ + x✝)) p✝ =
    ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝¹ + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝) p✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
⊢ 0 ≤ 0 ∧ 0 ≤ 1 ∧ 0 + 1 = 1 ∧ 0 = 0 • (0 + v₂) ∧ v₂ = 1 • (0 + v₂)

Tactic:
simp

Goal state after:
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₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x✝¹ • x✝)) p✝ =
    ((RingHom.id R) x✝¹ • (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x✝) p✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ : M
⊢ 0 ≤ 1 ∧ 0 ≤ 0 ∧ 1 + 0 = 1 ∧ v₁ = 1 • (v₁ + 0) ∧ 0 = 0 • (v₁ + 0)

Tactic:
simp

Goal state after: