mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T)

Tactic:
refine ⟨.trans _ (ULift.{max u₁ u₂ u₃} S) _, ?_⟩

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₁} R)).Flat
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ hI.dpow m (hI.dpow x✝ x) = hI'.dpow m (hI.dpow x✝ x)

Tactic:
rw [hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ (baseChangeMkQ C (map f N).toSubmodule).ker = fBC.ker

Tactic:
map_toSubmodule f N

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB : Function.Surjective ⇑fAB
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ (baseChangeMkQ C (baseChangeMkQ B N.toSubmodule).ker).ker = fBC.ker
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
f g : PowerSeries R
n : ℕ
⊢ (powerSeriesFamily x (f + g)) n = (powerSeriesFamily x f + powerSeriesFamily x g) n

Tactic:
by_cases hx : 0 < x.orderTop <;> · simp [hx, add_smul]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : ℕ
hi : i ∈ image (fun i ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support
his : i ∉ ((powerSeriesFamily x (a * b)).coeff g).support
⊢ (PowerSeries.coeff i) (a * b) • (x ^ i).coeff g = 0

Tactic:
simpa [h, PowerSeries.coeff_mul, sum_smul] using his

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos.refine_1
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
⊢ Set.MapsTo (fun x ↦ ⟨x.1 + x.2, x⟩) ↑⋯.toFinset
    ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)

Tactic:
intro ij hij

Goal state after:
case pos.refine_1
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
ij : ℕ × ℕ
hij : ij ∈ ↑⋯.toFinset
⊢ (fun x ↦ ⟨x.1 + x.2, x⟩) ij ∈ ↑((image (fun i ↦ i.1 + i.2) ⋯.toFinset).sigma HasAntidiagonal.antidiagonal)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
i : Fin (Nat.succ 0).succ
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] i = (MvPowerSeries.map f) (![g₁, g₂] i)

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨0, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨1, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : gh ∉ (fun a ↦ a) '' ↑(VAddAntidiagonal g ⋯)
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh
    by_cases h : s.hsum.coeff gh.1 = 0
    · exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)
    · simp_all

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ IsLocalHom (Ideal.Quotient.mk I)

Tactic:
constructor
  intro a h
  have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) := by
    rw [isUnit_iff_exists_inv] at *
    obtain ⟨b, hb⟩ := h
    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
    use Ideal.Quotient.mk _ b
    rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
    exact h hb
  obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this
  obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
  rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
    Ideal.mem_jacobson_bot] at h1 h2
  specialize h1 1
  have h1 : IsUnit a ∧ IsUnit y := by simpa using h1
  exact h1.1

Goal state after:
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hpq : p < q
Q : Ideal S
hPQ : P ≤ Q
hQ : Q.IsPrime
hQq : Q.LiesOver q
⊢ ∃ Q, P < Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
refine ⟨Q, lt_of_le_of_ne hPQ fun h ↦ ?_, hQ, hQq⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hpq : p < q
Q : Ideal S
hPQ : P ≤ Q
hQ : Q.IsPrime
hQq : Q.LiesOver q
h : P = Q
⊢ False
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ ofConv 1 = ofConv 1 ∘ₗ f.toLinearMap

Tactic:
← convOne_comp_coalgHom f.toCoalgHom

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ ofConv 1 ∘ₗ f.toLinearMap = ofConv 1 ∘ₗ f.toLinearMap
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
I K : Ideal A
hK : K ∈ G
hIK : F.IsTorsionQuot I K
J L : Ideal A
hL : L ∈ G
hJL : F.IsTorsionQuot J L
⊢ ∃ z ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K}, (fun x1 x2 ↦ x1 ≥ x2) I z ∧ (fun x1 x2 ↦ x1 ≥ x2) J z

Tactic:
refine ⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩

Goal state after:
case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
I K : Ideal A
hK : K ∈ G
hIK : F.IsTorsionQuot I K
J L : Ideal A
hL : L ∈ G
hJL : F.IsTorsionQuot J L
⊢ I ⊓ J ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mem_of_le
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
⊢ ∀ {x y : Ideal A}, x ≤ y → x ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K} → y ∈ {L | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
· intro I J hIJ ⟨K, hK, hIK⟩
    exact ⟨K, hK, hIK.mono_left hIJ⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (map (algebraMap R (Localization p.primeCompl)) (span ↑s)).minimalPrimes
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ m < n + 1,
              ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
                p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (maximalIdeal (Localization p.primeCompl)).height ≤ ↑(n + 1)

Tactic:
map_span

Goal state after:
case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (span (⇑(algebraMap R (Localization p.primeCompl)) '' ↑s)).minimalPrimes
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ m < n + 1,
              ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
                p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (maximalIdeal (Localization p.primeCompl)).height ≤ ↑(n + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
⊢ ∀ (q : Ideal R),
    q.IsPrime → q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height < ↑n + 1

Tactic:
ENat.lt_natCast_add_one_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
⊢ ∀ (q : Ideal R),
    q.IsPrime → q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ ↑n
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : IsLasker R M
N : Submodule R M
⊢ ∃ t, N.IsMinimalPrimaryDecomposition t

Tactic:
obtain ⟨s, hs1, hs2⟩ := h N
  obtain ⟨t, h1, h2, h3, h4⟩ :=
    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs1 hs2
  exact ⟨t, h1, h2, h3, h4⟩

Goal state after:
Module: Mathlib.RingTheory.LocalIso

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_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
g : S
hg : g ∈ {g | IsStandardOpenImmersion R (Localization.Away g)}
⊢ TensorProduct.includeRight g ∈ {g | IsStandardOpenImmersion T (Localization.Away g)}

Tactic:
simp only [Set.mem_ofPred_eq] at hg ⊢

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
⊢ IsStandardOpenImmersion T (Localization.Away (TensorProduct.includeRight g))
Module: Mathlib.RingTheory.LocalIso

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_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ IsLocalIso T (T ⊗[R] S)

Tactic:
by
  rw [iff_span_isStandardOpenImmersion_eq_top, _root_.eq_top_iff,
    ← Ideal.map_top Algebra.TensorProduct.includeRight, ← span_isStandardOpenImmersion_eq_top R S,
    Ideal.map_le_iff_le_comap, Ideal.span_le]
  intro g hg
  apply Ideal.subset_span
  simp only [Set.mem_ofPred_eq] at hg ⊢
  exact .of_algEquiv <| IsLocalization.Away.tensorProductEquivTMulRight R T g (Localization.Away g)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ }.asIdeal ^ d ∣ Ideal.span {f}
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f

Tactic:
Ideal.span_singleton_pow,

Goal state after:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Ideal.span {PowerSeries.X ^ d} ∣ Ideal.span {f}
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
hn : n ∈ Submonoid.pi Set.univ fun i ↦ Submonoid.map (Pi.evalRingHom R i) M
⊢ ∃ m ∈ M, n ∣ m

Tactic:
by
    choose m mem eq using hn
    have := Fintype.ofFinite ι
    refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩
    rw [Fintype.prod_apply]
    exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(↑(renameSymmetricSubalgebra e) ((aeval fun i ↦ ⟨esymm σ R (↑i + 1), ⋯⟩) (X i))) =
    ↑((aeval fun i ↦ ⟨esymm τ R (↑i + 1), ⋯⟩) (X i))

Tactic:
aeval_X,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑(↑(renameSymmetricSubalgebra e) ⟨esymm σ R (↑i + 1), ⋯⟩) = esymm τ R (↑i + 1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r * esymm (Fin m) R (↑i + 1) ^ b✝) = r

Tactic:
((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r

case add_single.hD
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ Function.Injective ⇑toLex

case add_single.hadd
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ), toLex (a1 + a2) = toLex a1 + toLex a2
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ antidiagonal k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ pairs σ k with #t.1 = a.1, f t = ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
by
  apply sum_finset_product
  simp only [mem_filter, mem_powersetCard_univ, mem_univ, and_true, and_iff_right_iff_imp]
  rintro p hp
  have : #p.fst ≤ k := by apply le_of_lt; simp_all
  aesop

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
S : Type u_4
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
φ : MvPowerSeries σ S
⊢ (expand p hp) ((substAlgHom hf) φ) = (substAlgHom ⋯) φ

Tactic:
by
  rw [← AlgHom.comp_apply, expand_comp_substAlgHom]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a ∈ antidiagonal k ∧ a.1 < k ∧ ¬0 < a.1 ↔ a ∈ {(0, k)}

Tactic:
mem_antidiagonal,

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1 ↔ a ∈ {(0, k)}
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ W_ R 0 = X 0

Tactic:
by
  simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]

Goal state after:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case refine_2
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
⊢ φ = wittStructureRat p Φ

Tactic:
funext n

Goal state after:
case refine_2
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = wittStructureRat p Φ n
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

Tactic:
replace H := (ih j hj).2 (vars_pow _ _ H)

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ range (j + 1)
⊢ i ∈ range n
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittZero p n = 0

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittZero p n) = (map (Int.castRingHom ℚ)) 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittOne p 0 = 1

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittOne p 0) = (map (Int.castRingHom ℚ)) 1
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ (map (Int.castRingHom ℚ)) (wittOne p n) = (map (Int.castRingHom ℚ)) 0