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

Goal state before:
pp: case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = Int.negSucc n • ∫ (x : ℝ) in 0..T, f x

Tactic:
conv_rhs => rw [negSucc_zsmul]

Goal state after:
case negSucc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -((n + 1) • ∫ (x : ℝ) in 0..T, f x)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ι 0 (2 * π)), ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖

Tactic:
· simp [norm_smul]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
⊢ CircleIntegrable f₂ c R

Tactic:
by_cases hR : R = 0
  · simp [hR]
  apply (intervalIntegrable_congr_codiscreteWithin _).1 hf₁
  rw [eventuallyEq_iff_exists_mem]
  exact ⟨(circleMap c R)⁻¹' {z | f₁ z = f₂ z},
    codiscreteWithin_mono (by simp only [Set.subset_univ]) (circleMap_preimage_codiscrete hR hf),
    by tauto⟩

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

Goal state before:
pp: case mpr
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| → CircleIntegrable (fun z ↦ (z - w) ^ n) c R

Tactic:
· rintro (rfl | H)
    exacts [circleIntegrable_zero_radius,
      ((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
        H.symm.imp_left fun (hw : w ∉ sphere c |R|) =>
          sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']

Goal state after:
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 ⋯
⊢ HasIntegral I GP (fun x ↦ (f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (I.face i) GP (fun x ↦ f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume -
      integral (I.face i) GP (fun x ↦ f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)

Tactic:
change HasIntegral I GP (fun x => f' x (Pi.single i 1)) _ (F I)

Goal state after:
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 ⋯
⊢ HasIntegral I GP (fun x ↦ (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (F I)
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 ν)
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) ∂ν)

Tactic:
simp [integral_sub h2f h2g]

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 μ
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) ∂ν)

Tactic:
simp [integral_sub h2f h2g]

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

Goal state before:
pp: case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
refine Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_

Goal state after:
case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ HasSum (fun n ↦ (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R θ))
    ((fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R θ))
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z

Tactic:
have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]

Goal state after:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ z ∈ sphere c R, ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * ↑π * I / ↑n.factorial ≠ 0
⊢ iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map (fun t ↦ -t) s).card

Tactic:
rwa [card_map]

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
o.analyticOn_iff_analyticOnNhd

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f 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
⊢ max B 1 ^ (p.natDegree - i) * ↑(p.natDegree.choose i) ≤ max B 1 ^ d * ↑(p.natDegree.choose i)

Tactic:
gcongr
        · apply le_max_right
        · exact le_trans (Nat.sub_le _ _) h3

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

Goal state before:
pp: p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
w : ℝ
hw : (aeval w) p = 0
⊢ (aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ) w)) p = 0

Tactic:
rw [aeval_algHom_apply, hw, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case refine_3
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 Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
x : O
⊢ (if h : ∃ x_1, v x_1 = v ((algebraMap O F) x) then ⟨v ((algebraMap O F) x), ⋯⟩ else 1) ≤ 1

Tactic:
simp [← Subtype.coe_le_coe, hv.map_le_one]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ 0 = (φ x).im

Tactic:
eq_comm,

Goal state after:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (φ x).im = 0
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
⊢ StrictMono (⇑ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul)

Tactic:
exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
⊢ closedBall x r ⊆ closedBall y s

Tactic:
have hx := closedBall_subset_closedBall hrs (x := x)

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
h : (closedBall x r ∩ closedBall y s).Nonempty
hxz : h.some ∈ closedBall x r
hyz : h.some ∈ closedBall y s
hx : closedBall x r ⊆ closedBall x s
⊢ closedBall x r ⊆ closedBall y s
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ IsOpen (ball x r)ᶜ

Tactic:
isOpen_iff

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ IsOpen (closedBall x r)

Tactic:
isOpen_iff

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε > 0, ball x_1 ε ⊆ closedBall x r
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

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

pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
⊢ (coeff d) φ = 0

Tactic:
· simp only [hφ, map_zero]

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

Goal state before:
pp: case h₀.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:
simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]

Goal state after:
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 : (if n ≤ i + n then r * (coeff (i + n - n)) p else 0) = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
if_pos le_add_self,

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 + n - n)) 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 : (if n ≤ i + n then (coeff (i + n - n)) p * r else 0) = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
if_pos le_add_self,

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 + n - n)) p * r = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ)

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)

case inr
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = 1 - constantCoeff φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : constantCoeff ↑ψ = f (constantCoeff φ)
this : IsUnit (constantCoeff ↑ψ)
⊢ IsUnit φ

Tactic:
rw [h] at this

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : constantCoeff ↑ψ = f (constantCoeff φ)
this : IsUnit (f (constantCoeff φ))
⊢ IsUnit φ
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ ≠ 0
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1

Tactic:
eq_comm,

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ ≠ 0
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z = Q x * P z

Tactic:
by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z = Q y * P z

Tactic:
by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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
⊢ (ConcreteCategory.hom (F.map h.op)) ((ConcreteCategory.hom (F.map (E.p₁ k).op)) (s i)) =
    (ConcreteCategory.hom (F.map h.op)) ((ConcreteCategory.hom (F.map (E.p₂ k).op)) (s 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
⊢ (ConcreteCategory.hom (F.map (E.p₁ k).op)) (s i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (s j)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![0, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ ¬(3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
⊢ have this := ⋯;
  (piComparison F fun x ↦ op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Tactic:
by
  have : HasCoproduct X := ⟨⟨c, hc⟩⟩
  dsimp only [Equalizer.Presieve.Arrows.forkMap]
  have h : Pi.lift (fun i ↦ F.map (c.inj i).op) =
      F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp
  rw [h, ← Category.assoc, ← Functor.map_comp]
  have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
    simp [Pi.lift, productIsProduct]
  rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]
  simp

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

Goal state before:
pp: case refine_1
X Y✝ : Scheme
𝓤 : Y✝.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y✝
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y✝ ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (𝓤.f j).op)) e = x (𝓤.f j) ⋯

Tactic:
dsimp [e]

Goal state after:
case refine_1
X Y✝ : Scheme
𝓤 : Y✝.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y✝
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y✝ ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
⊢ 𝓤.f j ≫ Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯ = x (𝓤.f j) ⋯
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve.ofArrows F.obj (colimit.ι F) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)

Tactic:
Sieve.ofArrows,

Goal state after:
J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
⊢ Sieve.generate (Presieve.ofArrows F.obj (colimit.ι F)) ≤ Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
congr! 1

Goal state after:
case e'_1
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (H1Cotangent R (Localization.Away f)) ∧
      Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R]

Tactic:
congr! 1

Goal state after:
case e'_1
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (H1Cotangent R (Localization.Away f)) ↔ Subsingleton (LocalizedModule.Away f (H1Cotangent R A))

case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R]