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

Goal state before:
pp: case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
← lt_div_iff₀ hy,

Goal state after:
case inr
x y : ℝ
h : x < 1 / y
hy : 0 < y
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩
    rw [← abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨by linarith, hy2'.le⟩), ←
      abs_of_nonneg (one_div_nonneg.mpr (sqrt_nonneg _)), ← sq_lt_sq, div_pow, one_pow,
      sq_sqrt hy3.le, lt_one_div (pow_pos hy4 _) hy3, ← inv_one_add_tan_sq hy4.ne', one_div,
      inv_inv, add_comm, add_lt_add_iff_left, sq_lt_sq, abs_of_pos hy1,
      abs_of_nonneg (tan_nonneg_of_nonneg_of_le_pi_div_two hy1.le hy2'.le)]
    exact Real.lt_tan hy1 hy2'

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
inner_eq_mul_norm_of_angle_eq_zero h

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 + 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivAt f f' x
⊢ slope f x y < f'

Tactic:
by
  simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.lt_slope_of_hasDerivAt hx hy hxy hfd.neg)

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd y hy)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd x hx))

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

Goal state before:
pp: case convert_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x' : 𝕜
h : x' ∈ {0}ᶜ
⊢ x' ∈ ((fun x ↦ eval x (X ^ n)) '' {k | eval k (derivative (X ^ n)) = 0})ᶜ

Tactic:
simpa [derivative_X_pow, hn, show n ≠ 0 by aesop] using fun _ ↦ Ne.symm h

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ‖↑z‖ ^ 2 < 1

Tactic:
by
  rw [sq_lt_one_iff_abs_lt_one, abs_norm]
  exact z.norm_lt_one

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g : 𝕜 → 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
⊢ MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x

Tactic:
exact meromorphicNFAt_smul_iff_right_of_analyticAt h₁g h₂g

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

Goal state before:
pp: 𝕜 : 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
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ g y = (((fun x_1 ↦ x_1 - x) ^ (meromorphicOrderAt f x).untop₀) y)⁻¹ • f y

Tactic:
Pi.pow_apply,

Goal state after:
𝕜 : 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
y : 𝕜
h₁y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
h₂y : y ∈ {x}ᶜ
⊢ g y = ((y - x) ^ (meromorphicOrderAt f x).untop₀)⁻¹ • f y
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
hx : x ∈ U
this : 0 x ≤ (MeromorphicOn.divisor f U) x
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
      MeromorphicOn.divisor_apply, untop₀_nonneg] at this

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
hx : x ∈ U
this : 0 ≤ meromorphicOrderAt f x
⊢ 0 ≤ meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∉ U
⊢ toMeromorphicNFOn f U x = f x

Tactic:
· simp [toMeromorphicNFOn, h.meromorphicOn, hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ divisor (toMeromorphicNFOn f U) U = divisor f U

Tactic:
by
  ext z
  by_cases hz : z ∈ U <;> simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]

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

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (∏ n ∈ insert σ s₁, f n) x = ∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x

Tactic:
Finset.prod_insert hσ,

Goal state after:
case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x = ∏ n ∈ insert σ s₁, meromorphicTrailingCoeffAt (f n) x

Tactic:
Finset.prod_insert hσ,

Goal state after:
case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

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

Tactic:
h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt f x).untop₀) h₂g h₃g,

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicTrailingCoeffAt (f ^ n) x = g x ^ n
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) univ

Tactic:
intro z hz
    rw [extractFactor z hd]
    right
    use d z, (∏ᶠ u, (· - u) ^ update d z 0 u)
    simp [analyticAt, ne_zero]

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

Goal state before:
pp: case neg
𝕜 : 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:
· grind [meromorphicTrailingCoeffAt_id_sub_const]

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

Goal state before:
pp: case refine_2
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
⊢ a = b

Tactic:
have ⟨h₂a, h₂b⟩ : a ∈ ball 0 R ∧ b ∈ ball 0 R := by constructor <;> (by_contra; aesop)

Goal state after:
case refine_2
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
z : ℂ
hz : z ∈ ball 0 R
a : ℂ
ha : a ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
b : ℂ
hb : b ∈ {σ | (canonicalFactor R σ ^ F σ) z = 0}
h₂a : a ∈ ball 0 R
h₂b : b ∈ ball 0 R
⊢ a = b
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case pos
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
t0 : ↑I
htn1 : t0 ≤ t n.succ
htn : ¬t0 ≤ t n
hf : f (t0, a) ∈ (q e).target
⊢ ↑(q e).symm (f (t0, a)) = g (t0, a)

Tactic:
apply (q e).injOn ((q e).map_target hf) (h_sub ⟨le_of_not_ge htn, htn1⟩)
      rw [(q e).right_inv hf, ← hpq e]; exact congr($g_lifts _).symm

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 : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
⊢ (f ^ n) y = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y

Tactic:
Pi.pow_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℤ
hn : ¬n = 0
h : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜'
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
y : 𝕜
hy : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • g y
⊢ f y ^ n = (y - x) ^ (n * (meromorphicOrderAt f x).untop₀) • (g ^ n) y
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
⊢ ∃ g, CanonicalDecomp f g R

Tactic:
let g := toMeromorphicNFOn φ (closedBall 0 R)

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
⊢ ∃ g, CanonicalDecomp f g R
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)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
x y : X
γ✝ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
he : ∀ (γ : Path x y), γ 0 = p ↑e
g : (γ : Path x y) → Path.Homotopic.Quotient (↑e) ((cov.liftPath ↑γ ↑e ⋯) 1) :=
  fun γ ↦ Path.Homotopic.Quotient.mk { toContinuousMap := cov.liftPath ↑γ ↑e ⋯, source' := ⋯, target' := ⋯ }
_i : Setoid (Path x y) := Path.Homotopic.setoid x y
γ γ' : Path x y
hγ : γ ≈ γ'
⊢ g γ ≍ g γ'

Tactic:
by
    refine .trans (heq_of_eq ?_) (Path.Homotopic.Quotient.cast_heq rfl
      (cov.liftPath_apply_one_eq_of_homotopicRel hγ _ (he γ) _))
    rw [← Path.Homotopic.Quotient.mk_cast, Path.Homotopic.Quotient.eq]
    exact cov.homotopicRel_liftPath hγ _ (by aesop) (by aesop)

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

Goal state before:
pp: case neg
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
x : ℂ
h₃x : ¬(divisor f (ball 0 R)) x = 0
h₁x : x ∈ ball 0 R
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

Tactic:
have h₂x : w ≠ x := by
      rintro rfl
      exact h₃x (by simp [(D.meromorphicOn.mono_set ball_subset_closedBall).divisor_apply h₁x, h₂w])

Goal state after:
case neg
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
x : ℂ
h₃x : ¬(divisor f (ball 0 R)) x = 0
h₁x : x ∈ ball 0 R
h₂x : w ≠ x
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x y : ℝ
z1 : ℂ
left✝ : z1 ∈ re ⁻¹' {x}
hz2 : (norm ∘ f) z1 = y
⊢ 0 ≤ y

Tactic:
simp only [← hz2, comp, norm_nonneg]

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

Goal state before:
pp: case inr.inr.inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
w : ℂ
hw : w.im = b
⊢ ‖f w‖ ≤ C'

pp: case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ 0 < C'

Tactic:
· exact (hle_b _ hw).trans hC'.le

Goal state after:
case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ 0 < C'
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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
⊢ ∃! F_1, F_1 a₀ = ↑(F a₀) ∧ p ∘ ⇑F_1 = ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)

Tactic:
refine ⟨.comp ⟨Subtype.val, by fun_prop⟩ F, ⟨rfl, ?_⟩, ?_⟩

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
⊢ p ∘ ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp F) =
    ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)

case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
⊢ ∀ (y : C(A, E)),
    (fun F_1 ↦ F_1 a₀ = ↑(F a₀) ∧ p ∘ ⇑F_1 = ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)) y →
      y = { toFun := Subtype.val, continuous_toFun := ⋯ }.comp F
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℂ
s : Set ℂ
f : ℂ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ (Δ[s] f) e = (iteratedFDerivWithin ℝ 2 f s e) ![1, 1] + (iteratedFDerivWithin ℝ 2 f s e) ![Complex.I, Complex.I]

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he
    Complex.orthonormalBasisOneI]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: case h
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |f a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M

Tactic:
rw [← hF_re] at hM

Goal state after:
case h
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |(fun z ↦ (F z).re) a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
have h : a ≠ b := by intro hab; simp [hab] at hμ0

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
by
  have hint : IntegrableOn f (Ι a b) μ := hf.integrableOn_of_subset_isCompact
    isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin
  have h : a ≠ b := by intro hab; simp [hab] at hμ0
  let s := uIoo a b
  have hs' : s ⊆ Ι a b := by intro x hx; rcases hx with ⟨h1, h2⟩; grind
  have hs_ev : s =ᵐ[μ] Ι a b := by simpa using! Ioo_ae_eq_Ioc
  have hμ0' : μ s ≠ 0 := by
    have hμ : μ s = μ (Ι a b) := by rw [measure_congr hs_ev]
    rwa [hμ]
  obtain ⟨c, hc, heq⟩ := exists_eq_setAverage (isConnected_uIoo h) (hf.mono uIoo_subset_uIcc_self)
    (hint.mono_set hs') (measure_ne_top_of_subset hs' hμfin) hμ0'
  exact ⟨c, hc, by rwa [← setAverage_congr hs_ev]⟩

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : |R| ≤ 0
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w

pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w

Tactic:
· simp_all [ball_eq_empty.2 hR]

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w