mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case hC
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
x✝ : k
⊢ ↑(((↑((renameEquiv k d).trans
                (H.aevalEquiv.trans
                  ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))).comp
          C)
        x✝) =
    ↑(((↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp C) x✝)

pp: case hX
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
i✝ : { j // j ≠ i }
⊢ ↑(↑((renameEquiv k d).trans
            (H.aevalEquiv.trans
              ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))
        (X i✝)) =
    ↑(↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩) (X i✝))

Tactic:
<;>

Goal state after:
case hC
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
x✝ : k
⊢ ↑(((↑((renameEquiv k d).trans
                (H.aevalEquiv.trans
                  ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))).comp
          C)
        x✝) =
    ↑(((↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp C) x✝)

case hX
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
i✝ : { j // j ≠ i }
⊢ ↑(↑((renameEquiv k d).trans
            (H.aevalEquiv.trans
              ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))
        (X i✝)) =
    ↑(↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩) (X i✝))
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsProper f ∧ IsAffineHom f

Tactic:
eq_isProper_inf_isAffineHom

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
⊢ closure ↑(smoothLocus f) = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
⊢ closure ↑(smoothLocus f) = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @Etale = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
ext X Y f
    rw [etale_iff, affineLocally_iff_forall_isAffineOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: case left
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ LocallyOfFiniteType f

pp: case right
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ FormallyUnramified f

Tactic:
<;>

Goal state after:
case left
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ LocallyOfFiniteType f

case right
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ FormallyUnramified f
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.fst s v =
    ((equalizerPullbackMapIso hf hg v).inv ≫
        equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)) ≫
      pullback.fst s v

pp: case h₁
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v =
    ((equalizerPullbackMapIso hf hg v).inv ≫
        equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)) ≫
      pullback.snd s v

Tactic:
<;>

Goal state after:
case h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.fst s v =
    ((equalizerPullbackMapIso hf hg v).inv ≫
        equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)) ≫
      pullback.fst s v

case h₁
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v =
    ((equalizerPullbackMapIso hf hg v).inv ≫
        equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)) ≫
      pullback.snd s v
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case e'_1
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
x✝ : K
⊢ ↑t = Set.range Subtype.val

pp: case e'_3.e'_2
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
⊢ ↑t = Set.range Subtype.val

pp: case e'_5
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
e_3✝ : (adjoin k ↑t).toField.toCommRing ≍ (adjoin k (Set.range Subtype.val)).toField.toCommRing
⊢ ↑t = Set.range Subtype.val

Tactic:
<;>

Goal state after:
case e'_1
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
x✝ : K
⊢ ↑t = Set.range Subtype.val

case e'_3.e'_2
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
⊢ ↑t = Set.range Subtype.val

case e'_5
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
e_1✝ : ↥(adjoin k ↑t) = ↥(adjoin k (Set.range Subtype.val))
e_3✝ : (adjoin k ↑t).toField.toCommRing ≍ (adjoin k (Set.range Subtype.val)).toField.toCommRing
⊢ ↑t = Set.range Subtype.val
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inl
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
obtain ⟨s, hs⟩ := IntermediateField.fg_top k K
    have : Algebra.IsAlgebraic (Algebra.adjoin k (s : Set K)) K := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      exact Algebra.isIntegral_of_surjective topEquiv.surjective
    obtain ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := k) (s : Set K)
    lift t to Finset K using s.finite_toSet.subset hts
    have : Algebra.IsAlgebraic (IntermediateField.adjoin k (t : Set K)) K := by
      convert! ht.isAlgebraic_field <;> simp
    exact ⟨t, ht, inferInstance⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr.hi
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k), (frobeniusEquiv k p).symm r = 0 → r = 0

pp: case inr.hj
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (m : K), (frobenius K p).toAddMonoidHom m = 0 → m = 0

pp: case inr.hc
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k) (m : K),
    (frobenius K p).toAddMonoidHom ((frobeniusEquiv k p).symm r • m) = r • (frobenius K p).toAddMonoidHom m

Tactic:
<;>

Goal state after:
case inr.hi
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k), (frobeniusEquiv k p).symm r = 0 → r = 0

case inr.hj
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (m : K), (frobenius K p).toAddMonoidHom m = 0 → m = 0

case inr.hc
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ ∀ (r : k) (m : K),
    (frobenius K p).toAddMonoidHom ((frobeniusEquiv k p).symm r • m) = r • (frobenius K p).toAddMonoidHom m
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map a)

pp: case e'_3
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map b)

Tactic:
<;>

Goal state after:
case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left a) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map a)

case e'_3
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
X Y : Over S
a b : X ⟶ Y
hab : (Over.pullback f).map a = (Over.pullback f).map b
e_1✝ : (pullback X.hom f ⟶ pullback Y.hom f) = (((Over.pullback f).obj X).left ⟶ ((Over.pullback f).obj Y).left)
⊢ pullback.map X.hom f Y.hom f (Over.Hom.left b) (𝟙 T) (𝟙 S) ⋯ ⋯ = Over.Hom.left ((Over.pullback f).map b)
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ IsStandardOpenImmersion R S

Tactic:
Algebra.isStandardOpenImmersion_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ ∃ r, Away r S
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
h : IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion R T

Tactic:
Algebra.isStandardOpenImmersion_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
h : ∃ r, Away r S
⊢ ∃ r, Away r T
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ map (algebraMap R S) p * C u = 0

Tactic:
have := h (f u) p (by rw [aeval_algHom_apply, ← map_mul, hp, map_zero])

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
this : map (algebraMap R T) p * C (f u) = 0
⊢ map (algebraMap R S) p * C u = 0
Module: Mathlib.RingTheory.RingHom.QuasiFinite

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_6⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).QuasiFinite → (algebraMap S (TensorProduct R S T)).QuasiFinite

Tactic:
introv H

Goal state after:
R S T : Type u_6
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).QuasiFinite
⊢ (algebraMap S (TensorProduct R S T)).QuasiFinite
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x c a : S
ha : a ∈ {a | ∀ (b : S), a * b ∈ R[x]}
b : S
⊢ c • a * b ∈ R[x]

Tactic:
by simpa only [smul_eq_mul, mul_left_comm, mul_assoc] using ha (c * b)

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H : (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p
⊢ (aeval x) (IsLocalization.integerNormalization M p) * t = 0

Tactic:
by simp [H, hp]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / 0 } = { toFractionRing := 0 }

Tactic:
div_zero

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ { toFractionRing := 0 } = { toFractionRing := 0 }
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ v ((aeval y) p) = 0

pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ p ≠ 0

Tactic:
<;>

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ v ((aeval y) p) = 0

Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ p ≠ 0
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case add
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p✝ q✝ : K[X]
a✝¹ : (Polynomial.aeval X) p✝ = (algebraMap K[X] K⟮X⟯) p✝
a✝ : (Polynomial.aeval X) q✝ = (algebraMap K[X] K⟮X⟯) q✝
⊢ (Polynomial.aeval X) (p✝ + q✝) = (algebraMap K[X] K⟮X⟯) (p✝ + q✝)

pp: case monomial
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
n✝ : ℕ
a✝ : K
⊢ (Polynomial.aeval X) ((Polynomial.monomial n✝) a✝) = (algebraMap K[X] K⟮X⟯) ((Polynomial.monomial n✝) a✝)

Tactic:
<;>

Goal state after:
case add
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p✝ q✝ : K[X]
a✝¹ : (Polynomial.aeval X) p✝ = (algebraMap K[X] K⟮X⟯) p✝
a✝ : (Polynomial.aeval X) q✝ = (algebraMap K[X] K⟮X⟯) q✝
⊢ (Polynomial.aeval X) (p✝ + q✝) = (algebraMap K[X] K⟮X⟯) (p✝ + q✝)

case monomial
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
n✝ : ℕ
a✝ : K
⊢ (Polynomial.aeval X) ((Polynomial.monomial n✝) a✝) = (algebraMap K[X] K⟮X⟯) ((Polynomial.monomial n✝) a✝)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
⊢ Polynomial.eval₂ f a x.num / 0 = 0

Tactic:
div_zero

Goal state after:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
⊢ 0 = 0
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos.inl
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a x.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

pp: case pos.inr
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

Tactic:
<;>

Goal state after:
case pos.inl
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a x.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

case pos.inr
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom