mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ ∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
exact integral_prod f hf

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝¹ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this✝ : Fact (ν V < ∞)
x : X
y : Y
hy : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ y ∈ V

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝¹ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this✝ : Fact (ν V < ∞)
x : X
y : Y
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝¹ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this✝ : Fact (ν V < ∞)
y : Y
x : X
hy : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ y ∈ V

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝¹ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this✝ : Fact (ν V < ∞)
y : Y
x : X
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

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
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t ↦ t • (w - z) + z
⊢ f z = f w

Tactic:
suffices g 0 = g 1 by simpa [g]

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun t ↦ t • (w - z) + z
⊢ g 0 = g 1
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w

Tactic:
have hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R) :=
    (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hne z hz

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) s.powerset).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)

Tactic:
← bind_powerset_len,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t))
        ((range (s.card + 1)).bind fun k ↦ powersetCard k s)).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)
Module: Mathlib.Analysis.Complex.CauchyIntegral

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

Tactic:
smul_inv_smul₀

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z

case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f✝ g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a✝ b✝ : ℝ × ℝ
hle : a✝ ≤ b✝
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f✝ (Set.Icc a✝ b✝)
Hcg : ContinuousOn g (Set.Icc a✝ b✝)
Hdf : ∀ x ∈ Set.Ioo a✝.1 b✝.1 ×ˢ Set.Ioo a✝.2 b✝.2 \ s, HasFDerivAt f✝ (f' x) x
Hdg : ∀ x ∈ Set.Ioo a✝.1 b✝.1 ×ˢ Set.Ioo a✝.2 b✝.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a✝ b✝) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
⊢ ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 ↦ x

Tactic:
convert!
          (((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
              (MeasurableEquiv.measurableEmbedding _) f _).symm

Goal state after:
case e'_3.e'_6
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f✝ g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a✝ b✝ : ℝ × ℝ
hle : a✝ ≤ b✝
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f✝ (Set.Icc a✝ b✝)
Hcg : ContinuousOn g (Set.Icc a✝ b✝)
Hdf : ∀ x ∈ Set.Ioo a✝.1 b✝.1 ×ˢ Set.Ioo a✝.2 b✝.2 \ s, HasFDerivAt f✝ (f' x) x
Hdg : ∀ x ∈ Set.Ioo a✝.1 b✝.1 ×ˢ Set.Ioo a✝.2 b✝.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a✝ b✝) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
⊢ Set.Icc (a 0) (b 0) = ⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Set.Icc a b
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mp
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
⊢ Nonempty v.RankOne → MulArchimedean (ofClass v).ValueGroup₀

Tactic:
intro h
    obtain hv := Nonempty.some h
    exact MulArchimedean.comap hv.hom'.toMonoidHom hv.strictMono'

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
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := (restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe)
⊢ Function.Bijective ⇑(galActionHom p ℂ)

Tactic:
refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩

Goal state after:
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 = ⊤
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
k : K
hk : embedding ((restrict₀ (ofClass v)) k) = embedding ↑x
⊢ v k ≠ 0

Tactic:
simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
k : K
hk : v k = embedding ↑x
⊢ v k ≠ 0
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
k : K
h0 : v k ≠ 0
hk : embedding ((restrict₀ (ofClass v)) k) = embedding ↑x
⊢ v k ≠ 1

Tactic:
simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
hx : x ≠ 1
k : K
h0 : v k ≠ 0
hk : v k = embedding ↑x
⊢ v k ≠ 1
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
⊢ StrictMono embedRealFun

Tactic:
intro x y h

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
⊢ embedRealFun x < embedRealFun y
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬x = 0
⊢ False

Tactic:
rw [← (valuation (K := K)).restrict.zero_iff, ← ne_eq, ← isUnit_iff_ne_zero] at hx0

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : IsUnit (valuation.restrict x)
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1

Tactic:
exact mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ (ofJ1728 R).IsElliptic

Tactic:
by
  rw [isElliptic_iff, ofJ1728_Δ]
  convert! (hu.out.pow 6).neg
  norm_num1

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
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = -0

Tactic:
Affine.Point.neg_zero

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = 0
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1
X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (x : ToType (uliftFunctor.obj X)), ∃ i y, (ConcreteCategory.hom (uliftFunctor.map (E.f i))) y = x

Tactic:
intro ⟨x⟩

Goal state after:
case refine_1
X : TopCat
E : precoverage.ZeroHypercover X
x : ↑X
⊢ ∃ i y, (ConcreteCategory.hom (uliftFunctor.map (E.f i))) y = { down := x }
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔ ((algebraMap S (Localization.Away r)).comp f).FormallyUnramified

Tactic:
rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
    formallyUnramified_algebraMap]

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

Goal state before:
pp: case intro.mp
R : Type u_1
I : Type u_2
inst✝³ : Finite I
f : I → Type u_3
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
⊢ FormallyUnramified R ((i : I) → f i) → ∀ (i : I), FormallyUnramified R (f i)

Tactic:
intro _ i

Goal state after:
case intro.mp
R : Type u_1
I : Type u_2
inst✝³ : Finite I
f : I → Type u_3
inst✝² : CommRing R
inst✝¹ : (i : I) → CommRing (f i)
inst✝ : (i : I) → Algebra R (f i)
val✝ : Fintype I
a✝ : FormallyUnramified R ((i : I) → f i)
i : I
⊢ FormallyUnramified R (f i)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
⊢ ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)

Tactic:
intro x y h

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h✝ : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
x y : L
h : x ∈ K⟮y⟯
⊢ (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblX P = 0

Tactic:
by
  apply eq_zero_of_ne_zero_of_mul_right_eq_zero hPz
  rw [dblX_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']
  ring1

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ (component (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) ((sumInv I M) x) = (map I (component R ι M j)) x

Tactic:
by
  apply induction_on I _ x (fun x ↦ ?_)
  rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ ((sumInv I M) x) j = (map I (component R ι M j)) x

Tactic:
by
  apply induction_on I _ x (fun x ↦ ?_)
  rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ Submodule.Quotient.mk (f x) = Submodule.Quotient.mk y0

Tactic:
← mkQ_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = Submodule.Quotient.mk y0
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = Submodule.Quotient.mk y0

Tactic:
← mkQ_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = (I ^ n • ⊤).mkQ y0
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n : ℕ
hn : m ≤ n
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m

Tactic:
induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hmn ih =>
    rw [← Ideal.Quotient.factorₐ_comp _
      (Ideal.pow_le_pow_right n.le_succ) (Ideal.pow_le_pow_right hmn), AlgHom.comp_assoc]
    simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
⊢ ⊤ ≤ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
rintro p -
  obtain ⟨m, rfl⟩ := hg p
  wlog h : m ∈ LinearMap.ker s
  · let x : M := f (s m)
    rw [show g m = g (m - f (s m)) by simp [hfg.apply_apply_eq_zero]]
    apply this hs hfg v hg hslzero hli hsp
    replace hs := DFunLike.congr_fun hs (s m)
    simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq] at hs
    simp [hs]
  have : m ∈ Submodule.span R (Set.range v) := hsp Submodule.mem_top
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
  simp only [LinearMap.mem_ker, Finsupp.sum, map_sum, map_smul,
    Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, map_add, hslzero, smul_zero,
    Finset.sum_const_zero, zero_add] at h
  replace hli := (linearIndependent_iff'.mp hli) c.support.toRight (c ∘ .inr) h
  simp only [Finset.mem_toRight, Finsupp.mem_support_iff, Function.comp_apply, not_imp_self] at hli
  simp only [Finsupp.sum, Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, hli, zero_smul,
    Finset.sum_const_zero, add_zero, map_sum, map_smul]
  exact Submodule.sum_mem _ (fun i hi ↦ Submodule.smul_mem _ _ <| Submodule.subset_span ⟨i, rfl⟩)

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

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = m + n

Tactic:
obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Goal state after:
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
P : SubmersivePresentation R S w✝³ w✝²
hP : P.dimension = n
⊢ ∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = m + n