mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
⊢ ∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
        ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)

Tactic:
simp only [← setIntegral_congr_set (Box.coe_ae_eq_Icc _)]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
hE : CompleteSpace E
⊢ ∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i, (f' x) (e i) i =
    ∑ x,
      ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * |2 * π - 0| = 2 * π * |R| * C

Tactic:
sub_zero,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
⊢ |R| * C * |2 * π| = 2 * π * |R| * C
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ ∮ (z : ℂ) in C(c, R), f' z = 0

Tactic:
rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
hi : CircleIntegrable f' c R
⊢ ∮ (z : ℂ) in C(c, R), f' z = (f ∘ circleMap c R) (2 * π) - (f ∘ circleMap c R) 0
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Tactic:
refine lintegral_congr_ae ?_

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᵐ[μ] fun x ↦ F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case h_closed
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : α × β), ↑↑f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ}

pp: case h_ae
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
· exact isClosed_eq continuous_integral continuous_integral_integral

Goal state after:
case h_ae
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᵐ[μ.prod ν] g →
      Integrable f (μ.prod ν) →
        ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ →
          ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry fun x ↦ ⇑(B x))

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun z ↦ (B (f z.1)) (g z.2)) (μ.prod ν)
⊢ ∫ (x : α), (B.flip (∫ (y : β), g y ∂ν)) (f x) ∂μ = (B (∫ (x : α), f x ∂μ)) (∫ (x : β), g x ∂ν)

Tactic:
ContinuousLinearMap.integral_comp_comm _ hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun z ↦ (B (f z.1)) (g z.2)) (μ.prod ν)
⊢ (B.flip (∫ (y : β), g y ∂ν)) (∫ (x : α), f x ∂μ) = (B (∫ (x : α), f x ∂μ)) (∫ (x : β), g x ∂ν)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
y : ↑(p.rootSet E)
⊢ ∃ a, mapRoots p E a = y

Tactic:
have key := (IsSplittingField.splits p.SplittingField p).roots_map
      (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)

Goal state after:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
y : ↑(p.rootSet E)
key :
  (map (↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p)).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
⊢ f x = g x

Tactic:
rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h

Goal state after:
case neg.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
⊢ f x = g x

case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
⊢ f x = g x
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x ::ₘ {y}).esymm 1 = x + y

Tactic:
by
  simp [esymm, powersetCard_one, add_comm]

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
⊢ Continuous g

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
⊢ (t ∩ (ball c R \ s)).Nonempty

Tactic:
obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty := by
    refine sdiff_nonempty.2 fun hsub => ?_
    have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
    rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
    exact this.not_gt Cardinal.aleph0_lt_continuum

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
x : ℝ
hx : x ∈ Ioo l u \ g ⁻¹' s
⊢ (t ∩ (ball c R \ s)).Nonempty
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Continuous fun x ↦ eval x p

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_1
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ mkRat m (k * a.den) ∈ ratLt x

Tactic:
rw [mkRat_mem_ratLt hka0, ← smul_smul]
      simpa using hm2

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 + k • a.num • 1 ≤ k • a.den • x + k • a.den • y
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
← sub_le_iff_le_add

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 + k • a.num • 1 - k • a.den • y ≤ k • a.den • x
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : (restrict₀ (ofClass v.restrict)) k = ↑x
⊢ (hom v) (v.restrict k) = (hom v) (embedding ((restrict₀ (ofClass v.restrict)) k))

Tactic:
congr 1

Goal state after:
case e_6
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : (restrict₀ (ofClass v.restrict)) k = ↑x
⊢ v.restrict k = embedding ((restrict₀ (ofClass v.restrict)) k)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ p.natDegree = p.natDegree + 0

Tactic:
add_zero

Goal state after:
p : ℝ[X]
hp : Irreducible p
z : ℂ
hz : (aeval z) p = 0
⊢ p.natDegree = p.natDegree
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ ‖x * y‖ = max ‖x‖ ‖y‖

Tactic:
← inv_inv x,

Goal state after:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ ‖x⁻¹⁻¹ * y‖ = max ‖x⁻¹⁻¹‖ ‖y‖
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
by
    have ne : Set.Nonempty (toLex '' φ.support) := (Function.support_nonempty_iff.mpr h).image _
    apply WithTop.some
    apply WellFounded.min _ (toLex '' φ.support) ne
    · exact Finsupp.instLTLex.lt
    · exact wellFounded_lt

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
this : r * (coeff (i + n - n)) p = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
add_tsub_cancel_right

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
this : r * (coeff i) p = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
this : (coeff (i + n - n)) p * r = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
add_tsub_cancel_right

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
this : (coeff i) p * r = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (-a *
      ∑ x ∈ antidiagonal (single () n),
        if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
congr 1

Goal state after:
case neg.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (∑ x ∈ antidiagonal (single () n),
      if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
      else 0) =
    ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
⊢ grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

Tactic:
by
  rw [grothendieckTopology, ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
W : C
p : W ⟶ E.Y k
hp : (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows p
⊢ t ((p ≫ E.p₁ k) ≫ E.f i) ⋯ = t ((p ≫ E.p₂ k) ≫ E.f j) ⋯

Tactic:
congr 1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
W : C
p : W ⟶ E.Y k
hp : (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows p
⊢ (p ≫ E.p₁ k) ≫ E.f i = (p ≫ E.p₂ k) ≫ E.f j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
Affine.evalEval_polynomialX

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      (W.toAffine.a₁ * (P y / P z) - (3 * (P x / P z) ^ 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0