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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f
hfi : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] 0

Tactic:
rcases le_total a b with hab | hab <;>
    simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢
  · exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi
  · rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ ∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x

Tactic:
apply integral_lt_integral_of_ae_le_of_measure_setOfPred_lt_ne_zero hab.le
    (hfc.intervalIntegrable_of_Icc hab.le) (hgc.intervalIntegrable_of_Icc hab.le)

Goal state after:
case hle
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ f ≤ᵐ[volume.restrict (Ioc a b)] g

case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ (volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n < ↑(n - d)! * ε
⊢ a * c ^ n / ↑(n - d)! < ε

Tactic:
div_lt_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))

Goal state after:
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n < ↑(n - d)! * ε
⊢ a * c ^ n < ↑(n - d)! * ε
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val

Tactic:
ext1 x

Goal state after:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
x : ↑(Ioc t (t + T))
⊢ ↑↑x = (QuotientAddGroup.mk ∘ Subtype.val) x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val

Tactic:
ext1 x

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
x : ↑(Ioc t (t + T))
⊢ ↑↑x = (QuotientAddGroup.mk ∘ Subtype.val) x
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
f : α × β → E
hf : AEStronglyMeasurable f (μ.prod ν)
⊢ (fun x ↦ ∫ (y : β), f (x, y) ∂ν) =ᵐ[μ] fun x ↦ ∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν

Tactic:
by
    filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx

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

Goal state before:

Tactic:
‖∮ z in C(c, R), f z‖ ≤ ∫ θ in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ :=
      intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
    _ < ∫ _ in 0..2 * π, R * C := by
      simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]
      refine intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
          Real.two_pi_pos ?_ continuousOn_const (fun θ _ => ?_) ⟨θ₀, Ioc_subset_Icc_self hmem, ?_⟩
      · exact continuousOn_const.mul (hc.comp (continuous_circleMap _ _).continuousOn fun θ _ =>
          circleMap_mem_sphere _ hR.le _).norm
      · gcongr
        exact hf _ <| circleMap_mem_sphere _ hR.le _
      · gcongr
    _ = 2 * π * R * C := by simp [mul_assoc]; ring

Goal state after:
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 μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
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) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

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 μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)
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 μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
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) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

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 μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
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 ν)
⊢ (fun x ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᵐ[μ] fun x ↦ F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

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 ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
⊢ ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b

Tactic:
ext1 x

Goal state after:
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
x : F
⊢ x ∈ ⇑eL ⁻¹' Set.Icc (eL a) (eL b) ↔ x ∈ Set.Icc a b
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}) =
    image (fun t ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
exact biUnion_singleton

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * (map (fun x ↦ x) x).prod

Tactic:
← prod_map_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (fun i ↦ Function.const R (-1) i * i) x).prod
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
⊢ IsReal (φ.comp f)

Tactic:
ext1 x

Goal state after:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case h
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := ⋯
this✝ : Algebra K ℂ := ⋯
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := ⋯
⊢ φ.comp ↑(ψ'.restrictNormal' K).symm.symm = ψ

Tactic:
ext1 x

Goal state after:
case h
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this✝ : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
x : K
⊢ (φ.comp ↑(ψ'.restrictNormal' K).symm.symm) x = ψ x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
⊢ IsReal (φ.comp (algebraMap k K))

Tactic:
ext1 x

Goal state after:
K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
x : k
⊢ (star (φ.comp (algebraMap k K))) x = (φ.comp (algebraMap k K)) x
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ (galActionHom p ℂ).range = ⊤

Tactic:
apply Equiv.Perm.subgroup_eq_top_of_swap_mem

Goal state after:
case h0
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Nat.Prime (Fintype.card ↑(p.rootSet ℂ))

case h1
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Fintype.card ↑(p.rootSet ℂ) ∣ Fintype.card ↥(galActionHom p ℂ).range

case h2
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ ?τ ∈ (galActionHom p ℂ).range

case h3
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Equiv.Perm.IsSwap ?τ

case τ
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Equiv.Perm ↑(p.rootSet ℂ)
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
hd : ball x r = ball y r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ

Tactic:
rw [hd] at hy
      simp [h.not_ge] at hy

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 : σ →₀ ℕ
h : ↑(toLex d) = φ.lexOrder
⊢ (coeff d) φ ≠ 0

Tactic:
by
  have hφ : φ ≠ 0 := by
    simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]
  have hφ' := lexOrder_def_of_ne_zero hφ
  rcases hφ' with ⟨ne, hφ'⟩
  simp only [← h, WithTop.coe_eq_coe] at hφ'
  suffices toLex d ∈ toLex '' φ.support by
    simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex] at this
    apply this
  rw [hφ']
  apply WellFounded.min_mem

Goal state after:
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‖
⊢ ‖∏ i ∈ s, f i‖ = s.sup' hs' fun i ↦ ‖f i‖

Tactic:
← coe_nnnorm',

Goal state after:
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‖
⊢ ↑‖∏ i ∈ s, f i‖₊ = s.sup' hs' fun i ↦ ‖f i‖
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≠ e

Tactic:
· rintro rfl
      simp_all

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
fst✝ u : σ →₀ ℕ
huv : (fst✝, u) ∈ antidiagonal e
a✝ : (fst✝, u) ≠ (0, e)
⊢ u ≠ e

Tactic:
· rintro rfl
      simp_all

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
h_inj : Set.InjOn maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ maximalIdeal '' {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}} ⊆ {v | v.asIdeal ∣ span {x}}

Tactic:
simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_ofPred_eq, subset_refl]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
⊢ ∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I

Tactic:
by
  conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
  simp only [← finprod_comp_equiv (equivHeightOneSpectrum (K := K)), equivHeightOneSpectrum_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
⊢ v ↑x * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x}) = 1

Tactic:
have hnz : span {x} ≠ ⊥ := mt Submodule.span_singleton_eq_bot.mp hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ v ↑x * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x}) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negMap ⟦P⟧ = ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧

Tactic:
rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]

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 }
this✝² : (E.sigmaOfIsColimit hc).HasPullbacks
this✝¹ : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
this✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
this : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
equiv : Nonempty (IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F)) ↔
  Nonempty (IsLimit (E.toPreOneHypercover.multifork F)) :=
  Equiv.nonempty_congr (E.isLimitSigmaOfIsColimitEquiv hc hc' F)
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
isLimit_toPreOneHypercover_type_iff,

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 }
this✝² : (E.sigmaOfIsColimit hc).HasPullbacks
this✝¹ : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
this✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
this : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
equiv : IsSheafFor F (E.sigmaOfIsColimit hc).presieve₀ ↔ Nonempty (IsLimit (E.toPreOneHypercover.multifork F))
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)
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 }
this✝² : (E.sigmaOfIsColimit hc).HasPullbacks
this✝¹ : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
this✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
this : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
equiv : IsSheafFor F (E.sigmaOfIsColimit hc).presieve₀ ↔ Nonempty (IsLimit (E.toPreOneHypercover.multifork F))
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
isLimit_toPreOneHypercover_type_iff,

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 }
this✝² : (E.sigmaOfIsColimit hc).HasPullbacks
this✝¹ : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
this✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
this : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
equiv : IsSheafFor F (E.sigmaOfIsColimit hc).presieve₀ ↔ IsSheafFor F E.presieve₀
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case 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 : P ≈ Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q

Tactic:
rcases h with ⟨u, rfl⟩
    exact ⟨Units.map f u, (comp_smul ..).symm⟩

Goal state after: