mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ 0

Tactic:
← hw

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C

Tactic:
set e := (lineMap z w : ℂ → E)

Goal state after:
case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ 0 ≤ deriv f b

Tactic:
← hw

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f w ≤ deriv f b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)

Tactic:
simpa [mul_comm x] using
    strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩
      pi_div_two_pos.ne (sub_pos.2 hx') hx

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
case inr => exact (sin_sq_lt_sq hx).le

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

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Tactic:
have hy : 0 < y := by
    have := mul_pos_iff.mp (zero_lt_one.trans h)
    simpa [hx, hx.asymm]
  have k := arctan_add (mul_inv x y ▸ inv_lt_one_of_one_lt₀ h)
  rw [arctan_inv_of_pos hx, arctan_inv_of_pos hy, show _ + _ = π - (arctan x + arctan y) by ring,
    sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', sub_eq_add_neg, ← arctan_neg, add_comm] at k
  grind

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

Goal state before:
pp: x : ℝ
⊢ ‖Complex.exp (Complex.I * ↑x) - 1‖ₑ ≤ ‖x‖ₑ

Tactic:
rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]

Goal state after:
x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖ₑ

Tactic:
rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]

Goal state after:
x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ENNReal.ofReal ‖x‖
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Tactic:
rintro _ ⟨z, ⟨hzs, hzx⟩, rfl⟩

Goal state after:
case refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ slope f x z ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case right.right
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
m : ℤ
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ m • g
⊢ f ^ n =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ (n * m) • g ^ n

Tactic:
filter_upwards [h₃g] with z hz
      simp [hz, mul_zpow, (zpow_mul' (z - x) n m).symm]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ Tendsto g (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))

Tactic:
rw [h₁g.meromorphicTrailingCoeffAt_of_eq_nhdsNE h₃g]
    apply h₁g.continuousAt.continuousWithinAt

Goal state after:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ Tendsto g (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x))

Tactic:
· rw [h₁g.meromorphicTrailingCoeffAt_of_eq_nhdsNE h₃g]
    apply h₁g.continuousAt.continuousWithinAt

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
n : ℤ
h₁f₁ : meromorphicOrderAt f₁ x = ↑n
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n • g z

Tactic:
filter_upwards [hf₁₂, h₃g] using by grind

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
rw [h₁]
    simp

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1

Tactic:
· rw [h₁]
    simp

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : (support d).Finite
u : 𝕜
h₁ : ¬u = x
⊢ u ∉ ↑h.toFinset → (x - u) ^ update d x 0 u = 1
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
hxy : x = y
⊢ meromorphicTrailingCoeffAt (fun x ↦ x - y) x ^ d y = (x - y) ^ update d x 0 y

Tactic:
rw [hxy, meromorphicTrailingCoeffAt_id_sub_const]
    simp_all

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
⊢ log (‖x - y‖ ^ update d x 0 y) = ↑(d y) * log ‖x - y‖

Tactic:
Real.log_zpow

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this✝ : ∀ y ∈ Finite.toFinset h, ‖(x - y) ^ update d x 0 y‖ ≠ 0
this : (support fun u ↦ ↑(d u) * log ‖x - u‖) ⊆ ↑(Finite.toFinset h)
y : 𝕜
hy : y ∈ Finite.toFinset h
⊢ ↑(update d x 0 y) * log ‖x - y‖ = ↑(d y) * log ‖x - y‖
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖

Tactic:
rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ meromorphicOrderAt (f ^ (n + 1)) x = ↑(n + 1) * meromorphicOrderAt f x

Tactic:
simp only [pow_add, pow_one, meromorphicOrderAt_mul (hf.pow n) hf, hn, Nat.cast_add,
      Nat.cast_one]
    cases meromorphicOrderAt f x
    · aesop
    · norm_cast
      simp only [Nat.cast_add, Nat.cast_one]
      ring

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

Tactic:
intro ⟨u, hu⟩
    rw [← (hg hu).meromorphicOrderAt_eq_zero_iff, ← meromorphicOrderAt_congr
        (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,
      meromorphicOrderAt_smul (hφ u hu).inv (h₁f u hu), meromorphicOrderAt_inv,
      meromorphicOrderAt_eq _ h₃f]
    simp only [h₁f, hu, divisor_apply]
    lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn
    rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]
    simp

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ ∀ (u : ↑U), g ↑u ≠ 0

pp: case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g

Tactic:
· -- ∀ (u : ↑U), g ↑u ≠ 0
    intro ⟨u, hu⟩
    rw [← (hg hu).meromorphicOrderAt_eq_zero_iff, ← meromorphicOrderAt_congr
        (toMeromorphicNFOn_eq_self_on_nhdsNE (hφ.inv.smul h₁f) hu).symm,
      meromorphicOrderAt_smul (hφ u hu).inv (h₁f u hu), meromorphicOrderAt_inv,
      meromorphicOrderAt_eq _ h₃f]
    simp only [h₁f, hu, divisor_apply]
    lift meromorphicOrderAt f u to ℤ using (h₂f ⟨u, hu⟩) with n hn
    rw [WithTop.untop₀_coe, ← WithTop.LinearOrderedAddCommGroup.coe_neg, ← WithTop.coe_add]
    simp

Goal state after:
case refine_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
h₃f : (divisor f U).support.Finite
φ : 𝕜 → 𝕜 := ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u
hφ : MeromorphicOn φ U
g : 𝕜 → E := toMeromorphicNFOn (φ⁻¹ • f) U
hg : MeromorphicNFOn g U
⊢ f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ (divisor f U) u) • g
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case mp.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
hn : Nonempty n
a : R
ha : (Matrix.scalar n) a = ↑g
b : R
hb : (Matrix.scalar n) b = ↑g⁻¹
⊢ g ∈ (scalar n).range

Tactic:
have hab : a * b = 1 := by
        simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g

Goal state after:
case mp.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
hn : Nonempty n
a : R
ha : (Matrix.scalar n) a = ↑g
b : R
hb : (Matrix.scalar n) b = ↑g⁻¹
hab : a * b = 1
⊢ g ∈ (scalar n).range
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : normSq (f z) = normSq z
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
normSq_apply (f z),

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).re * (f z).re + (f z).im * (f z).im = normSq z
⊢ (f z).im = z.im ∨ (f z).im = -z.im
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE

Tactic:
by
  have h0 : f I = I ∨ f I = -I := by
    simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
    constructor
    · rw [← I_re]
      exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
    · apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
      intro z
      rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
  refine h0.imp (fun h' : f I = I => ?_) fun h' : f I = -I => ?_ <;>
    · apply LinearIsometryEquiv.toLinearEquiv_injective
      apply Complex.basisOneI.ext'
      intro i
      fin_cases i <;> simp [h, h']

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e

Tactic:
induction n with

Goal state after:
case succ
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
ih : ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
⊢ ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t (n + 1))) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t (n + 1))) ∧ Γ 0 = e
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x✝ : ↑I
h✝ : ¬↑x✝ ≤ 1 / 2
⊢ p
      ({ toContinuousMap := cov.liftPath (↑γ') ((cov.liftPath (↑γ) e ⋯) 1) ⋯, source' := ⋯, target' := ⋯ }
        ⟨2 * ↑x✝ - 1, ⋯⟩) =
    γ' ⟨2 * ↑x✝ - 1, ⋯⟩

Tactic:
· refine congr_fun (cov.liftPath_lifts γ' _ ?_) _
    simpa using congr($(cov.liftPath_lifts γ ..) 1).symm

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
t : ↑I
a : A
⊢ (p ∘ fun ta ↦ (cov.liftPath (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) ta.2))) (f ta.2) ⋯) ta.1)
      (t, a) =
    H (t, a)

Tactic:
exact congr_fun (cov.liftPath_lifts ..) t

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x y : X
γ γ' : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
eq : ⋯.monodromy γ e = ⋯.monodromy γ' e
⊢ ⋯.monodromy γ = ⋯.monodromy γ'

Tactic:
by
    ext e'
    obtain ⟨g, rfl⟩ := hp.exists_toPermFiber_eq e e'
    simp_rw [monodromy_toPermFiber, eq]

Goal state after:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
⊢ log ‖h w‖ =
    ∑ᶠ (i : ℂ), ↑((divisor f (ball 0 R)) i) * log ‖canonicalFactor R i w‖ -
        ∑ᶠ (i : ℂ), ↑((divisor f (sphere 0 R)) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
by
  -- Finiteness properties and side results used throughout the proof
  let B₀R := ball (0 : ℂ) R
  let S₀R := sphere (0 : ℂ) R
  lift (divisor f S₀R).support to Finset ℂ using divisor_sphere_support_finite with t₁ ht₁
  lift (divisor f B₀R).support to Finset ℂ using D.meromorphicOn.divisor_ball_support_finite
    with t₂ ht₂
  calc Real.log ‖h w‖
    _ = log ‖((∏ᶠ (i : ℂ), canonicalFactor R i w ^ (divisor f B₀R) i)
        * ∏ᶠ (i : ℂ), (w - i) ^ (-divisor f S₀R) i) • meromorphicTrailingCoeffAt f w‖ := by
      rw [D.eq_smul_meromorphicTrailingCoeffAt_of_meromorphicOrderAt
        h₁w h₂w hR, finprod_eq_prod_of_mulSupport_subset (s := t₂) _ (by aesop)]
    _ = log ‖((∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i)
        * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i) • meromorphicTrailingCoeffAt f w‖ := by
      rw [finprod_eq_prod_of_mulSupport_subset (s := t₂) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₁) _ _]
      <;> simpa [ht₁, ht₂] using mulSupport_pow_subset_support ..
    _ =  ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i)
        + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) + log ‖meromorphicTrailingCoeffAt f w‖ := by
      have η₀ (x) (hx : x ∈ t₁) : ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0 := by
        refine zpow_ne_zero _ ?_
        rw [norm_ne_zero_iff, sub_ne_zero]
        rintro rfl
        simp_all [divisor_def, ← Finset.mem_coe]
      have η₁ (x) (hx : x ∈ t₂) : ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0 := by
        refine zpow_ne_zero _ ?_
        rw [norm_ne_zero_iff]
        have h₁x : x ∈ ball 0 R := (divisor f B₀R).supportWithinDomain (ht₂ ▸ hx)
        refine canonicalFactor_ne_zero h₁x h₁w fun _ ↦ ?_
        simp_all [divisor_def, ← Finset.mem_coe]
      simp_rw [norm_smul, norm_mul, norm_prod, norm_zpow]
      rw [Real.log_mul (mul_ne_zero_iff.2 ⟨Finset.prod_ne_zero_iff.2 η₁,
          Finset.prod_ne_zero_iff.2 η₀⟩) ?_, Real.log_mul (Finset.prod_ne_zero_iff.2 η₁)
        (Finset.prod_ne_zero_iff.2 η₀), Real.log_prod η₁, Real.log_prod η₀]
      simpa using (D.meromorphicOn w h₁w).meromorphicTrailingCoeffAt_ne_zero (by simp [h₂w])
    _ = ((∑ᶠ i, (divisor f B₀R i) * Real.log ‖canonicalFactor R i w‖)
        - (∑ᶠ i, (divisor f S₀R i) * Real.log ‖w - i‖))
        + Real.log ‖meromorphicTrailingCoeffAt f w‖ := by
      rw [finsum_eq_sum_of_support_subset (s := t₂) _ ?η₀,
        finsum_eq_sum_of_support_subset (s := t₁) _ ?η₁]
      case η₀ | η₁ => intro _ _; simp_all [S₀R, B₀R]
      rw [sub_eq_add_neg, ← Finset.sum_neg_distrib]
      congr! 3 with i hi i hi <;> simp

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n

Tactic:
by
    simp_rw [OrthonormalBasis.sum_inner_mul_inner v]

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
n : ℕ
m : Fin (n + 1) → V
f : E
⊢ ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
n : ℕ
y : V
f : E
⊢ ∂^{fun x ↦ y} f = ∂_{y}^[n] f

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
n : ℕ
m : Fin n → V
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
n : ℕ
m : Fin n → V
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousLineDeriv V E E
n : ℕ
m : Fin n → V
⊢ Continuous ∂^{m}

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
i : ℝ
i_pos : 0 < i
hi : ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f (↑x.re + ↑y * I) - f z‖ ≤ ε

Tactic:
exact ⟨i, i_pos, fun w w_in_ball y y_in_I ↦ hi (mem_closedBall_aux w_in_ball y_in_I)⟩

Goal state after: