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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ R * (2 * (π * C)) = 2 * (π * (R * C))

Tactic:
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 α
inst✝¹ : NormedAddCommGroup E
f : α → E
hf : MemLp f 1 μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ MemLp (fun x ↦ f x.1) 1 (μ.prod ν)

Tactic:
exact hf.comp_fst ν

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    0

Tactic:
refine (integral_boundary_rect_of_hasFDerivAt_real_off_countable f
    (fun z => (fderiv ℂ f z).restrictScalars ℝ) z w s hs Hc
    (fun x hx => (Hd x hx).hasFDerivAt.restrictScalars ℝ) ?_).trans ?_ <;>
      simp

Goal state after:
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)
hq : iteratedDeriv n f c = n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z
⊢ ‖n.factorial • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ ≤
    ↑n.factorial * (R * (C / R ^ (n + 1)))

Tactic:
by
      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp

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

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖deriv (⇑e ∘ f) c‖

Tactic:
this.deriv

Goal state after:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖e (deriv f c)‖
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymm σ R 0 = 1

Tactic:
by
  simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ (2 * ↑π * I) • 0 = 0

Tactic:
smul_zero

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

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

Tactic:
simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *

Goal state after:
case inl
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 : a ≤ b
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a
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
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
w : ↑(p.rootSet ℂ)
⊢ (AlgEquiv.restrictScalars ℚ conjAe) ↑w = ↑w ↔ (↑w).im = 0

Tactic:
exact Complex.conj_eq_iff_im

Goal state after:
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
⊢ (p.aroots ℂ).Nodup

Tactic:
· exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ unit v ≠ 1

Tactic:
by
  rw [Ne, ← Units.val_inj, Units.val_one]
  exact ((nontrivial v).choose_spec).2

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

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - (C z + C ((starRingEnd ℂ) z)) * X + C z * C ((starRingEnd ℂ) z) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
ring

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

Goal state before:
pp: case a
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
⊢ 0 ≤ embedRealFun 0

Tactic:
rw [le_csSup_iff (ratLt'_bddAbove (0 : M)) (ratLt'_nonempty 0)]
    intro x
    rw [mem_upperBounds]
    suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
    intro h
    have h' (y : ℚ) (hy : y < 0) : y ≤ x := by
      exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one
    contrapose! h'
    obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
    exact ⟨y, by simpa using hy, hxy⟩

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

Goal state before:
pp: case neg.inr.refine_2
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖

Tactic:
exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

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
⊢ φ.lexOrder = ⊤ ↔ φ = 0

Tactic:
by
  unfold lexOrder
  split_ifs with h
  · simp only [h]
  · simp only [h, WithTop.coe_ne_top]

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

Goal state before:
pp: σ : 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
⊢ (coeff e) x * constantCoeff φ = (coeff (e, 0).1) x * (coeff (e, 0).2) φ

pp: case h₀
σ : 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
⊢ ∀ b ∈ antidiagonal e, b ≠ (e, 0) → (coeff b.1) x * (coeff b.2) φ = 0

pp: case h₁
σ : 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
⊢ (e, 0) ∉ antidiagonal e → (coeff (e, 0).1) x * (coeff (e, 0).2) φ = 0

Tactic:
coeff_zero_eq_constantCoeff

Goal state after:
σ : 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
⊢ (coeff e) x * constantCoeff φ = (coeff (e, 0).1) x * constantCoeff φ

case h₀
σ : 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
⊢ ∀ b ∈ antidiagonal e, b ≠ (e, 0) → (coeff b.1) x * (coeff b.2) φ = 0

case h₁
σ : 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
⊢ (e, 0) ∉ antidiagonal e → (coeff (e, 0).1) x * (coeff (e, 0).2) φ = 0
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y z : L
⊢ v.norm (x - z) ≤ v.norm (x - y) + v.norm (y - z)

Tactic:
simp only [← sub_add_sub_cancel x y z]

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y z : L
⊢ v.norm (x - y + (y - z)) ≤ v.norm (x - y) + v.norm (y - z)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : 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
⊢ constantCoeff φ * (coeff e) x = (coeff (0, e).1) φ * (coeff (0, e).2) x

pp: case h₀
σ : 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
⊢ ∀ b ∈ antidiagonal e, b ≠ (0, e) → (coeff b.1) φ * (coeff b.2) x = 0

pp: case h₁
σ : 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
⊢ (0, e) ∉ antidiagonal e → (coeff (0, e).1) φ * (coeff (0, e).2) x = 0

Tactic:
coeff_zero_eq_constantCoeff

Goal state after:
σ : 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
⊢ constantCoeff φ * (coeff e) x = constantCoeff φ * (coeff (0, e).2) x

case h₀
σ : 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
⊢ ∀ b ∈ antidiagonal e, b ≠ (0, e) → (coeff b.1) φ * (coeff b.2) x = 0

case h₁
σ : 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
⊢ (0, e) ∉ antidiagonal e → (coeff (0, e).1) φ * (coeff (0, e).2) x = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : 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
⊢ constantCoeff φ * (coeff e) x = ∑ p ∈ antidiagonal e, (coeff p.1) φ * (coeff p.2) x

Tactic:
rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]

Goal state after:
case h₀
σ : 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
⊢ ∀ b ∈ antidiagonal e, b ≠ (0, e) → (coeff b.1) φ * (coeff b.2) x = 0

case h₁
σ : 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
⊢ (0, e) ∉ antidiagonal e → (coeff (0, e).1) φ * (coeff (0, e).2) x = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
⊢ (weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
⊢ ¬((weightedHomogeneousComponent w p) f = 0 ∨ (weightedHomogeneousComponent w q) g = 0)
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ IsPrincipalIdealRing ↥(valuation K v).integer

Tactic:
rw [(Valuation.integer.integers (v.valuation K)).isPrincipalIdealRing_iff_not_denselyOrdered,
    WithZero.denselyOrdered_set_iff_subsingleton]

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑(valuation K v)).Subsingleton
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ (coeff 0) f = f 0

Tactic:
coeff_zero_eq_constantCoeff

Goal state after:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ constantCoeff f = f 0
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
⊢ (fun i ↦
      match i with
      | WalkingMulticospan.left i => s.val i
      | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j))) ∈
    I.multicospan.sections

Tactic:
rintro _ _ (_ | _ | r)
        · rfl
        · rfl
        · exact (s.property r).symm

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f)

Tactic:
by
  rw [Presieve.isSheafFor_iff_generate]
  apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))
  · rw [← Sieve.generate_le_iff, Sieve.generate_sieve, Sieve.generate_le_iff,
      Presieve.ofArrows_le_iff]
    intro i
    rw [← f.w₀]
    exact ⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩
  · rwa [← Presieve.isSheafFor_iff_generate]
  · intro Y f hf
    rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate,
      ← Presieve.ofArrows_pullback]
    apply H₂

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.Nonsingular (W.add P Q)

pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
· simp only [add_of_Z_eq_zero hP hQ hPz hQz,
        nonsingular_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, nonsingular_zero]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k✝ : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
k a : E.toPreOneHypercover.I₁'
⊢ c'.inj a ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k✝)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k✝) =
    c'.inj a ≫
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k✝ ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
by simp; simp [c']

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦Q⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift ⟦Q⟧
hQz : Q z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![0, 1, 0] Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![0, 1, 0] P
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
a : E.toPreOneHypercover.I₁'
⊢ c'.inj a ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
    c'.inj a ≫
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
by simp; simp [c']

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S

Tactic:
by
  rw [FormallyUnramified, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
this : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (e i) = 1
⊢ (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) 1 = 1

Tactic:
simp [ι, ← he', this]

Goal state after: