mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]

Goal state after:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ Real.sin
      (if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + π else Real.arcsin ((-x).im / ‖x‖) - π) =
    x.im / ‖x‖

Tactic:
split_ifs

Goal state after:
case pos
x : ℂ
h✝ : 0 ≤ x.re
⊢ Real.sin (Real.arcsin (x.im / ‖x‖)) = x.im / ‖x‖

case pos
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : 0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) + π) = x.im / ‖x‖

case neg
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : ¬0 ≤ x.im
⊢ Real.sin (Real.arcsin ((-x).im / ‖x‖) - π) = x.im / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:

Tactic:
exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
x✝ : x ∈ univ
⊢ log (-rexp x) = x

Tactic:
log_neg_eq_log,

Goal state after:
x : ℝ
x✝ : x ∈ univ
⊢ log (rexp x) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x

Tactic:
· simp [zero_le_one]

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
obtain ⟨x, y⟩ := z
    rintro ⟨rfl : x = 0, hy : 0 < y⟩
    rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
· simp [zero_le_one]

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case negSucc
x : ℝ
a✝ : ℕ
⊢ -(↑(a✝ + 1) * log x) = ↑(Int.negSucc a✝) * log x

Tactic:
Int.cast_negSucc,

Goal state after:
case negSucc
x : ℝ
a✝ : ℕ
⊢ -(↑(a✝ + 1) * log x) = -↑(a✝ + 1) * log x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
n : ℤ
⊢ log (x ^ n) = ↑n * log x

Tactic:
cases n
  · rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]
  · rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]

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

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + 0 • ↑(2 * π / ↑2) ∨ ψ = θ + ↑1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
Fin.val_one,

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + 0 • ↑(2 * π / ↑2) ∨ ψ = θ + 1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
simp [Set.preimage, h]

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

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log ‖z‖) + ↑π * I))

Tactic:
by
  simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using
    (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto

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

Goal state before:
pp: x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs

Goal state after:
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Tactic:
split_ifs

Goal state after:
case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1

case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1

case neg
x : ℂ
h✝ : ¬1 = 0
⊢ cexp (log 1 * x) = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)

Tactic:
split_ifs

Goal state after:
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 1 = 1

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 1 = 0

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 1 = cexp (log 1 * z)

case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 1 = 1

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 1 = 0

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 1 = cexp (log 0 * z)

case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 0 = 1

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 0 = 0

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 0 = cexp (log 1 * z)

case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 0 = 1

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 0 = 0

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 0 = cexp (log 0 * z)

case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : cexp (log x * y) = 0
h✝ : z = 0
⊢ cexp (log x * (y * z)) = 1

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : cexp (log x * y) = 0
h✝ : ¬z = 0
⊢ cexp (log x * (y * z)) = 0

case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝¹ : ¬x = 0
h✝ : ¬cexp (log x * y) = 0
⊢ cexp (log x * (y * z)) = cexp (log (cexp (log x * y)) * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹

Tactic:
split_ifs

Goal state after:
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (-(log x * y)) = (cexp (log x * y))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Tactic:
split_ifs

Goal state after:
case pos
x : ℂ
h✝ : x.arg = π
⊢ |π| = |x.arg|

case neg
x : ℂ
h✝ : ¬x.arg = π
⊢ |(-x.arg)| = |x.arg|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case mp.refine_1
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

pp: case mp.refine_2
θ : ℝ
⊢ cexp (↑(toIocMod ⋯ (-π) θ) * I) = cexp (↑θ * I)

Tactic:
· convert! toIocMod_mem_Ioc _ _ _
      ring

Goal state after:
case mp.refine_2
θ : ℝ
⊢ cexp (↑(toIocMod ⋯ (-π) θ) * I) = cexp (↑θ * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r

Tactic:
rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]

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

Goal state before:
pp: θ : Angle
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

Tactic:
induction θ using Real.Angle.induction_on
  rw [toReal_coe]
  exact toIocMod_toIocMod _ _ _ _

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 Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 1 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 1 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 1 = rexp (log x * y)

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 0 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 0 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ¬↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 0 = rexp (log x * y)

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : ¬↑x = 0
h✝ : ¬x = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
rcases two_nsmul_eq_zero_iff.mp h with h | h

Goal state after:
case inl
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = 0
⊢ |θ.toReal| + |ψ.toReal| = π

case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs

Goal state after:
case pos
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℝ
hx : 0 ≤ x
h✝ : ¬x = 0
⊢ rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
split_ifs

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 ≤ 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ 0 ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ rexp (log (-x) * y)

Tactic:
log_neg_eq_log,

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
hψ : θ ≠ ↑π ∨ ψ ≠ ↑π
hs : θ.sign = -ψ.sign
h : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inr.inl
θ ψ : Angle
hψ : θ ≠ ↑π ∨ ψ ≠ ↑π
hs : θ.sign = -ψ.sign
h : ψ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inr.inr
θ ψ : Angle
hψ : θ ≠ ↑π ∨ ψ ≠ ↑π
hs : θ.sign = -ψ.sign
h : ψ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
all_goals grind [neg_neg, add_comm, toReal_add_of_sign_pos_sign_neg]

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

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : ¬y = 0
⊢ 1 = 0⁻¹

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : y = 0
⊢ 0 = 1⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ rexp (log x * -y) = (rexp (log x * y))⁻¹
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 (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)

Tactic:
split_ifs

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ ↑1 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ ↑0 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ ↑(rexp (Real.log x * y)) = cexp (log ↑x * ↑y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]
  exact Real.rpow_eq_zero_iff_of_nonneg x.2

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

Goal state before:
pp: y : ℝ
⊢ ((if 0 < y then 0 else if y = 0 then 1 else ∞) * if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
split_ifs

Goal state after:
case pos
y : ℝ
h✝ : 0 < y
⊢ 0 * 0 = 0

case pos
y : ℝ
h✝¹ : ¬0 < y
h✝ : y = 0
⊢ 1 * 1 = 1

case neg
y : ℝ
h✝¹ : ¬0 < y
h✝ : ¬y = 0
⊢ ∞ * ∞ = ∞
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:
by
  obtain hx | hx := le_or_gt x 0
  · exact hx.trans_lt (rpow_pos_of_pos hy _)
  · exact (lt_rpow_iff_log_lt hx hy).2 h

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    neg_vsub_eq_vsub_rev]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ f x = 0

Tactic:
by rw [hx, map_zero]

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✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun x ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 ((fun x ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' (convexHull 𝕜) s ⊆ (convexHull 𝕜) (⇑f '' s)

Tactic:
rw [Set.image_subset_iff]
    refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
    rw [← Set.image_subset_iff]
    exact subset_convexHull 𝕜 (f '' s)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) ≤ affineSpan 𝕜 s

Tactic:
affineSpan_le

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ [x -[𝕜] y] ⊆ s.pi fun i ↦ [x i -[𝕜] y i]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -

Goal state after:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i ↦ [x i -[𝕜] y i]) i
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ openSegment 𝕜 x y ⊆ s.pi fun i ↦ openSegment 𝕜 (x i) (y i)

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -

Goal state after:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y z : (i : ι) → M i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i ↦ openSegment 𝕜 (x i) (y i)) i
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
⊢ (sInf t).direction ≤ ⨅ s ∈ t, s.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (if 0 ∈ s then univ else ∅)

Tactic:
split_ifs

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
h✝ : 0 ∈ s
⊢ StrictConvex 𝕜 univ

case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
h✝ : 0 ∉ s
⊢ StrictConvex 𝕜 ∅
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₂ -ᵥ p₁) = v

Tactic:
by
  rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ((map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)

Tactic:
by
  simp_rw [weightedVSubOfPoint_apply]
  exact Finset.sum_map _ _ _

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ ((affineCombination k (Finset.subtype pred s) fun i ↦ p ↑i) fun i ↦ w ↑i) =
    (affineCombination k ({x ∈ s | pred x}) p) w

Tactic:
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]

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

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs w, ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p ↑i -ᵥ b)) →
    ∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)

Tactic:
rintro ⟨fs, w, rfl, rfl⟩

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∃ fs_1,
    ↑fs_1 ⊆ s ∧ ∃ w_1, ∑ i ∈ fs_1, w_1 i = ∑ i ∈ fs, w i ∧ ∑ i ∈ fs, w i • (p ↑i -ᵥ b) = ∑ i ∈ fs_1, w_1 i • (p i -ᵥ b)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ (affineCombination k s p) (affineCombinationLineMapWeights i j c) = (AffineMap.lineMap (p i) (p j)) c

Tactic:
by
  rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_piSingle k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case inr.inr.hd
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ (affineSpan k (s ×ˢ t)).direction = ((affineSpan k s).prod (affineSpan k t)).direction

pp: case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty

Tactic:
· simp [direction_prod_eq, Set.nonempty_iff_ne_empty.mp, hs, ht, direction_affineSpan,
      vectorSpan_prod_eq]

Goal state after:
case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b < r₁ * r₂

Tactic:
rw [mul_comm, mul_comm r₁]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ p b * ‖a‖ < r₂ * r₁