mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝² : x ∈ Box.Icc J
x✝¹ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
j : Fin n
x✝ : j ∈ Finset.univ
⊢ δ + δ ≤ 1 / 2 + 1 / 2

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_4.refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 2 * ↑c * ε' * volume.toBoxAdditive J ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
gcongr

Goal state after:
case c0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := ⋯
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := ⋯
F : Fin (n + 1) →ᵇᵃ[↑I] E := ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 0 ≤ volume.toBoxAdditive J

case h₂
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := ⋯
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := ⋯
F : Fin (n + 1) →ᵇᵃ[↑I] E := ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ volume.toBoxAdditive J ≤ (volume.toBoxAdditive.restrict ↑I ⋯) J
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun z ↦ y) (sphere c r)

Tactic:
· exact continuousOn_const

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ Bornology.IsBounded (range f)

Tactic:
obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
⊢ Bornology.IsBounded (range f)
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ t ∪ tᶜ ⊆ t ∪ s

Tactic:
gcongr

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymmPart σ R (Nat.Partition.indiscrete n) = esymm σ R n

Tactic:
cases n <;> simp [esymmPart]

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this✝ : w ∈ closure (ball c ↑R \ s)
this :
  HasFPowerSeriesOnBall (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c
    ↑R
⊢ w ∈ eball c ↑R

Tactic:
rwa [Metric.eball_coe]

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

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in b..a, f' x = f a - f b

Tactic:
exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ (Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val).prod.coeff k =
    (Multiset.map X univ.val).esymm (s.card - k)

Tactic:
convert! Multiset.prod_X_add_C_coeff s h

Goal state after:
case e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.commSemiring.toSemiring
⊢ Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r ↦ Polynomial.X + Polynomial.C r) s
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i) ≤ max B 1 ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

Tactic:
gcongr

Goal state after:
case hab
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ≤ max B 1
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ (p.natDegree - i) * ↑(p.natDegree.choose i) ≤ max B 1 ^ d * ↑(p.natDegree.choose i)

Tactic:
gcongr

Goal state after:
case ha
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ 1 ≤ max B 1

case hmn
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ p.natDegree - i ≤ d
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ d * ↑(p.natDegree.choose i) ≤ max B 1 ^ d * ↑(d.choose (d / 2))

Tactic:
gcongr

Goal state after:
case a
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ p.natDegree.choose i ≤ d.choose (d / 2)
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : CommRing O
inst✝ : Algebra O F
v✝ : Valuation F Γ₀
v : F →*₀ Γ₀
a : F
ha : 0 < v a
b c : F
hbc : v b < v c
⊢ v a * v b < v a * v c

Tactic:
gcongr

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 : M
⊢ BddAbove (ratLt x)

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch x zero_lt_one

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 : M
n : ℕ
hn : x ≤ n • 1
⊢ BddAbove (ratLt x)
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
hxy : x < y
⊢ (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) y

Tactic:
rwa [(WithZero.map'_strictMono (MulEquiv.strictMono_symm (mulintEquivOfZPowersEqTop_strictMono
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)
    (Left.one_lt_inv_iff.mpr hv.generator'_lt_one)))).lt_iff_lt]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case ofNat
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.ofNat a✝‖₊ ≤ ‖x‖₊

Tactic:
simpa using nnnorm_pow_le _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case negSucc
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.negSucc a✝‖₊ ≤ ‖x‖₊

Tactic:
simpa using nnnorm_pow_le _ _

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
hφ : φ ≠ 0
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Tactic:
simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, WithTop.ne_top_iff_exists] at hφ
  obtain ⟨p, hp⟩ := hφ
  exact ⟨ofLex p, by simp only [toLex_ofLex, hp]⟩

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
⊢ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0

Tactic:
d

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
⊢ ↑(toLex d) < w → (coeff d) φ = 0
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ ∀ (x y : ℝ≥0), ↑(max x y) = max ↑x ↑y

Tactic:
by tauto

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

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
⊢ (C r)⁻¹ = C r⁻¹

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Goal state after:
case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ (C 0)⁻¹ = C 0⁻¹

case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (C r)⁻¹ = C r⁻¹
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
· intro I f hI hfX hfI
      rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
      have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
      rw [← Ideal.eq_top_iff_one]
      apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
i j : (E.sigmaOfIsColimit hc).I₀
⊢ HasPullback ((E.sigmaOfIsColimit hc).f i) ((E.sigmaOfIsColimit hc).f j)

Tactic:
dsimp [sigmaOfIsColimit]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
i j : (E.sigmaOfIsColimit hc).I₀
⊢ HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
⊢ FamilyOfElements F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)

Tactic:
by tauto

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
⊢ FamilyOfElements.Compatible fun ⦃Y⦄ f a ↦ ⋯.elim

Tactic:
by tauto

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
Y : Type w
t : F.obj (op I)
h :
  (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) t ∧
    ∀ (y : F.obj (op I)), (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) y → y = t
a : Y ⟶ F.obj (op I)
x✝ : Y
⊢ (fun t ↦ FamilyOfElements.IsAmalgamation (fun ⦃Y⦄ f a ↦ ⋯.elim) t) ((ConcreteCategory.hom a).toFun x✝)

Tactic:
by tauto

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some X Y ⋯

Tactic:
by
  simp only [toAffine_of_Z_ne_zero h one_ne_zero, fin3_def_ext, div_one]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x) * f (Q z) = f (Q x) * f (P z)

pp: case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y) * f (Q z) = f (Q y) * f (P z)

Tactic:
exacts [X_eq_of_equiv h, Y_eq_of_equiv h]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (piComparison F fun x ↦ op (X x))

Tactic:
rw [piComparison_fac (hc := hc)]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso
    (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialZ = (MvPolynomial.map f) W'.polynomialZ

Tactic:
simp only [polynomialZ, map_polynomial, pderiv_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ⊓ IsOpenImmersion.precoverage ≤
    Precoverage.comap forgetToTop
        (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage) ⊓
      Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
gcongr

Goal state after:
case h₁
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ≤
    Precoverage.comap forgetToTop (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage)

case h₂
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case h₁
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ≤
    Precoverage.comap forgetToTop (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage)

Tactic:
← Precoverage.comap_comp,

Goal state after:
case h₁
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ≤
    Precoverage.comap (forgetToTop ⋙ CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
xj : ↑(𝒰.X j)
hj : (ConcreteCategory.hom (𝒰.f j)) xj = y
this :
  (ConcreteCategory.hom ((yoneda.obj X).map (pullbackCone (𝒰.f i) (𝒰.f j)).fst.op)) (x i) =
    (ConcreteCategory.hom ((yoneda.obj X).map (pullbackCone (𝒰.f i) (𝒰.f j)).snd.op)) (x j)
⊢ (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨(ConcreteCategory.hom (𝒰.f i)) xi, ⋯⟩) =
    (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨(ConcreteCategory.hom (𝒰.f j)) xj, ⋯⟩)

Tactic:
dsimp at this

Goal state after:
case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
xj : ↑(𝒰.X j)
hj : (ConcreteCategory.hom (𝒰.f j)) xj = y
this : (pullbackCone (𝒰.f i) (𝒰.f j)).fst ≫ x i = (pullbackCone (𝒰.f i) (𝒰.f j)).snd ≫ x j
⊢ (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨(ConcreteCategory.hom (𝒰.f i)) xi, ⋯⟩) =
    (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨(ConcreteCategory.hom (𝒰.f j)) xj, ⋯⟩)