mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
⊢ (divisor (f₁ + f₂) U)⁻ x = (divisor f₁ U)⁻ x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∉ U
⊢ (divisor (f₁ + f₂) U)⁻ x = (divisor f₁ U)⁻ x

Tactic:
· suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
      simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]
    by_cases h : 0 ≤ meromorphicOrderAt f₁ x
    · suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
      calc 0
      _ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
        le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg
      _ ≤ meromorphicOrderAt (f₁ + f₂) x :=
        meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt
    · suffices meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x by
        rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
      calc meromorphicOrderAt f₁ x
      _ < 0 := by simpa using h
      _ ≤ meromorphicOrderAt f₂ x := (hf₂ x hx).meromorphicOrderAt_nonneg

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∉ U
⊢ (divisor (f₁ + f₂) U)⁻ x = (divisor f₁ U)⁻ x
Module: Mathlib.Analysis.Meromorphic.Divisor

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

Tactic:
by
  ext x
  by_cases hx : x ∈ U
  · suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
      simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]
    by_cases h : 0 ≤ meromorphicOrderAt f₁ x
    · suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
      calc 0
      _ ≤ min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) :=
        le_inf h (hf₂ x hx).meromorphicOrderAt_nonneg
      _ ≤ meromorphicOrderAt (f₁ + f₂) x :=
        meromorphicOrderAt_add (hf₁ x hx) (hf₂ x hx).meromorphicAt
    · suffices meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x by
        rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
      calc meromorphicOrderAt f₁ x
      _ < 0 := by simpa using h
      _ ≤ meromorphicOrderAt f₂ x := (hf₂ x hx).meromorphicOrderAt_nonneg
  simp [hx]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update f x (Classical.choose ⋯ x) x = 0 ^ n • g x

Tactic:
simp_rw [hn]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
⊢ Function.update f x (Classical.choose ⋯ x) x = 0 ^ 0 • g x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq✝ : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
z : 𝕜
hg_eq : (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
hz : z ∈ {x}ᶜ
⊢ f z = (z - x) ^ (↑m - ↑(Exists.choose hf)) • g z

Tactic:
rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul,
        ← zpow_add₀ (sub_ne_zero.mpr hz), ← add_sub_assoc, add_sub_cancel_left, zpow_natCast,
        zpow_natCast]

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 𝕜
g : 𝕜 → 𝕜
h₁g : AnalyticOnNhd 𝕜 g U
h₂g : ∀ u ∈ U, g u ≠ 0
⊢ MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U

Tactic:
constructor <;> intro h z hz
  · rw [← meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g z hz) (h₂g z hz)]
    exact h hz
  · apply (h hz).smul_analytic (h₁g z hz)
    exact h₂g z hz

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : 0 ≤ meromorphicOrderAt f x
⊢ ∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)

Tactic:
by
  rcases ho.eq_or_lt with ho | ho
  · rcases tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho.symm with ⟨c, -, hc⟩
    exact ⟨c, hc⟩
  · exact ⟨0, tendsto_zero_of_meromorphicOrderAt_pos ho⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
⊢ (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)

Tactic:
simp [mulSupport]

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 c : 𝕜
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x - c) x = meromorphicTrailingCoeffAt f (x - c)

Tactic:
simp [sub_eq_add_neg, ← meromorphicTrailingCoeffAt_comp_add_const_eq_meromorphicTrailingCoeffAt]

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ 0 ≤ divisor φ⁻¹ U + divisor f U

pp: 𝕜 : 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
⊢ ∀ z ∈ U, meromorphicOrderAt φ⁻¹ z ≠ ⊤

Tactic:
divisor_inv,

Goal state after:
case refine_1
𝕜 : 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
⊢ 0 ≤ -divisor φ U + divisor f U

𝕜 : 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
⊢ ∀ z ∈ U, meromorphicOrderAt φ⁻¹ z ≠ ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

Tactic:
rw [← Finset.add_sum_erase _ _ (by aesop : z ∈ h.toFinset), Finset.sum_eq_zero (by aesop)]

Goal state after:
case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (F z * if z ∈ U then (single z 1) z else 0) + 0 = F z
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t : ↑I
⊢ ∀ (a' : ↑I), p (((fun st ↦ (Γ st.2) st.1) ∘ fun y ↦ (1, y)) t) = p (((fun st ↦ (Γ st.2) st.1) ∘ fun y ↦ (1, y)) a')

Tactic:
t'

Goal state after:
case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t t' : ↑I
⊢ p (((fun st ↦ (Γ st.2) st.1) ∘ fun y ↦ (1, y)) t) = p (((fun st ↦ (Γ st.2) st.1) ∘ fun y ↦ (1, y)) t')
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
⊢ g ∈ (scalar n).range

Tactic:
obtain ⟨a, ha⟩ := mem_center_iff_val_mem_range_scalar.mp hg
      obtain ⟨b, hb⟩ := mem_center_iff_val_mem_range_scalar.mp (Subgroup.inv_mem _ hg)
      have hab : a * b = 1 := by
        simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g
      refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
      simp [Units.ext_iff, ← ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
u : GL n R
hu : u ∈ Subgroup.center (GL n R)
⊢ u ∈ Subgroup.comap (map f) (Subgroup.center (GL n S))

Tactic:
by
  simp only [GeneralLinearGroup.center_eq_range_scalar, MonoidHom.mem_range,
    Subgroup.mem_comap] at hu ⊢
  obtain ⟨r, rfl⟩ := hu
  exact ⟨(Units.map f) r, GeneralLinearGroup.map_scalar _ _ |>.symm⟩

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
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n_max))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n_max))
Γ_0 : Γ 0 = e
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Tactic:
rw [h_max _ le_rfl] at cont eqOn

Goal state after:
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
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) → ∃ u, meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
· intro h₂f
    obtain ⟨v, hv⟩ := hU.nonempty
    use ⟨v, hv⟩, h₂f ⟨v, hv⟩

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)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t✝ : ↑I
a : A
ha : a ∈ S
t : ↑I
⊢ ∀ (a' : ↑I),
    p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t✝, a).2))) (f₀' (t✝, a).2) ⋯)
          t) =
      p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t✝, a).2))) (f₀' (t✝, a).2) ⋯)
          a')

Tactic:
t'

Goal state after:
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
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t✝ : ↑I
a : A
ha : a ∈ S
t t' : ↑I
⊢ p ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t✝, a).2))) (f₀' (t✝, a).2) ⋯) t) =
    p
      ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t✝, a).2))) (f₀' (t✝, a).2) ⋯)
        t')
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt (f ∘ fun x ↦ x - c) x = meromorphicOrderAt f (x - c)

Tactic:
simp_rw [sub_eq_add_neg, ← meromorphicOrderAt_comp_add_const_eq_meromorphicOrderAt]

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

Goal state before:
pp: x : ℝ
⊢ IsOpen {z | z.im < x}

Tactic:
by
  simpa using isOpen_im_lt_EReal x

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

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

Tactic:
simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]

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

Goal state before:
pp: c w : ℂ
⊢ poissonKernel c w = re ∘ herglotzRieszKernel c w

Tactic:
ext z
  rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)

Tactic:
rw [div_le_div_iff₀]

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) * (R - r) ≤ (R + r) * (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

case hb
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)

case hd
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R - r
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
⊢ ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = ∮ (z : ℂ) in C(0, R), (↑q / (↑q * z - W)) • f z

Tactic:
apply circleIntegral.integral_congr hR.le fun z hz ↦ ?_

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
z : ℂ
hz : z ∈ sphere 0 R
⊢ z⁻¹ • (↑q * z / (↑q * z - W)) • f z = (↑q / (↑q * z - W)) • f z
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case neg.inr.refine_2.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x ↦ 1) (Ioc 0 c) μ
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) (Ioc 0 c) μ

Tactic:
refine IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc

Goal state after:
case neg.inr.refine_2.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : 0 ≤ c
this : IntegrableOn (fun x ↦ 1) (Ioc 0 c) μ
x : ℝ
hx : x ∈ Ioc 0 c
⊢ 1 = ‖↑x ^ r‖
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case pos
x y : ℝ
ha : ¬x = 0
hb : y = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

pp: case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
· simp [hb, posLog]

Goal state after:
case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: x : ℝ
| log (sin x)

Tactic:
← sin_pi_sub

Goal state after:
x : ℝ
| log (sin (π - x))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: b : ℝ
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
rcases lt_trichotomy b 0 with h | h | h
  · -- If t is negative, use that log is an even function to reduce to the positive case.
    conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
    rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
      integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
    ring
  · simp [h]
  · exact integral_log_from_zero_of_pos h

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

Goal state before:
pp: r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
| (circleMap 0 r₁ θ * (starRingEnd ℂ) (circleMap 0 ‖ρ‖ ρ.arg)).re

Tactic:
conj_circleMap_zero,

Goal state after:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
| (circleMap 0 r₁ θ * circleMap 0 ‖ρ‖ (-ρ.arg)).re
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
⊢ Tendsto (fun x ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
apply (tendsto_nhdsWithin_of_tendsto_nhds hcts.tendsto).congr'
  filter_upwards [self_mem_nhdsWithin] with a using cuspFunction_eq_of_nonzero h f

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

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]

Goal state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ ‖↑(z - c).re‖ < (↑(z - c).re).re + 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
have := @integral_sin_pow_odd_mul_cos_pow a b 0 2
  norm_num at this; exact this

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ |g (e x) - f x| = -‖f‖ / 3 - f x

Tactic:
by
          rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.right
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ (scalar (Fin 2)) (m.discr / 4) = 0

Tactic:
rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]

Goal state after:
case mpr.right
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
⊢ ((diagonal fun x ↦ a) + n - (scalar (Fin 2)) ((∑ i, a + n.trace) / 2)) ^ 2 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ g.fixpointPolynomial = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
fixpointPolynomial

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
this : a ≠ 0
⊢ (↑n * a ^ (n - 1)) • m ≠ 0

Tactic:
by simp [this, hm0, hn]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
i j : { a // (a ≠ k) = True }
⊢ (auxMat M k).toSquareBlock (fun x ↦ x ≠ k) True i j = (M k k • 1) i j

Tactic:
simp [auxMat, toSquareBlock_def, if_neg (of_eq_true i.2), if_neg (of_eq_true j.2),
    Matrix.one_apply, Subtype.ext_iff]

Goal state after: