mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) f) = (algebraMap B (B ⧸ Q)) 0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0

Tactic:
rwa [map_zero, hq, ← hr, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_X,
      mul_eq_zero, or_iff_right (pow_ne_zero _ hbQ)] at hf

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b (∑ k ∈ Finset.range k, (monomial (k + 1)) (f.coeff (k + 1 + j))) + f.coeff (0 + j) * b ^ 0 - a ∈ g • Q

Tactic:
zero_add,

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b (∑ k ∈ Finset.range k, (monomial (k + 1)) (f.coeff (k + 1 + j))) + f.coeff j * b ^ 0 - a ∈ g • Q
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb : (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
hg : g • Q = Q
⊢ (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) b₀

Tactic:
hx g hg

Goal state after:
case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb : (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
hg : g • Q = Q
⊢ (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) b₀ = (algebraMap B (B ⧸ Q)) a * (algebraMap B (B ⧸ Q)) b₀
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1

pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1

Tactic:
· intro h; apply h

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b

Tactic:
· rintro ⟨u, rfl⟩
    obtain rfl | rfl := Int.units_eq_one_or u
    · exact Or.inl (by simp)
    · exact Or.inr (by simp)

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
x✝ : MulSemiringAction (↥(MulAction.stabilizer G Q)) L := MulSemiringAction.compHom L (stabilizerHom G P Q K L)
f : Gal(L/K)
g : ↥(MulAction.stabilizer G Q)
hg :
  (MulSemiringAction.toAlgAut (↥(MulAction.stabilizer G Q)) (↥(FixedPoints.subfield (↥(MulAction.stabilizer G Q)) L)) L)
      g =
    AlgEquiv.ofRingEquiv ⋯
⊢ (stabilizerHom G P Q K L) g = f

Tactic:
AlgEquiv.ext_iff

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
x✝ : MulSemiringAction (↥(MulAction.stabilizer G Q)) L := MulSemiringAction.compHom L (stabilizerHom G P Q K L)
f : Gal(L/K)
g : ↥(MulAction.stabilizer G Q)
hg :
  ∀ (a : L),
    ((MulSemiringAction.toAlgAut (↥(MulAction.stabilizer G Q)) (↥(FixedPoints.subfield (↥(MulAction.stabilizer G Q)) L))
            L)
          g)
        a =
      (AlgEquiv.ofRingEquiv ⋯) a
⊢ ∀ (a : L), ((stabilizerHom G P Q K L) g) a = f a
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x ↦ g ^ x) n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a

Tactic:
subst a; intro h
    rw [← Nat.card_eq_fintype_card] at hodd h
    have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) := by
      rw [← pow_mul] at h
      rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
      apply orderOf_dvd_of_pow_eq_one h
    have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
    obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
    refine ⟨g ^ m, ?_⟩
    dsimp
    rw [mul_comm, pow_mul, pow_two]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ (algebraMap R L) (r₁ * r₂) = IsLocalization.mk' L r₁ s

Tactic:
IsLocalization.mk'_eq_mul_mk'_one,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ (algebraMap R L) (r₁ * r₂) = (algebraMap R L) r₁ * IsLocalization.mk' L 1 s
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ 0 ∣ absNorm (span {x})

Tactic:
← hI

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z

Tactic:
← mul_one x,

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x * 1 = ↑z
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R₀ M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R₀ R M
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
⊢ IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M

Tactic:
by
  refine IsSemiprimaryRing.induction R₀ R M (P := fun M ↦ IsNoetherian R M ∨ IsArtinian R M →
    Module.Finite R₀ M) (fun M _ _ _ _ _ hJ h ↦ ?_) (fun M _ _ _ _ hs hq h ↦ ?_)
  · let _ := hJ.module
    have := IsSemisimpleModule.finite_tfae (R := R) (M := M)
    simp_rw [this.out 1 0, this.out 2 0, or_self,
      hJ.semilinearMap.finite_iff_of_bijective Function.bijective_id] at h
    exact .trans (R ⧸ Ring.jacobson R) M
  · let N := (Ring.jacobson R • ⊤ : Submodule R M).restrictScalars R₀
    have : Module.Finite R₀ N := by refine hs (h.imp ?_ ?_) <;> (intro; infer_instance)
    have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)
    exact .of_submodule_quotient N

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
q : Ideal S
inst✝² : q.LiesOver p
inst✝¹ : p.IsMaximal
inst✝ : q.IsMaximal
⊢ Module.finrank (R ⧸ p) (S ⧸ q) = q.inertiaDeg R

Tactic:
inertiaDeg_eq_of_isMaximal p q

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
q : Ideal S
inst✝² : q.LiesOver p
inst✝¹ : p.IsMaximal
inst✝ : q.IsMaximal
⊢ Module.finrank (R ⧸ p) (S ⧸ q) = Module.finrank (R ⧸ p) (S ⧸ q)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : I ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro f₁ f₂ e
  let := f₁.toRingHom.toAlgebra
  have := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm
  have :=
    ((KaehlerDifferential.linearMapEquivDerivation R A).toEquiv.trans
          (derivationToSquareZeroEquivLift I hI)).surjective.subsingleton
  exact Subtype.ext_iff.mp (@Subsingleton.elim _ this ⟨f₁, rfl⟩ ⟨f₂, e.symm⟩)

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing T
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
r : R
m : T
h : r • m = 0
⊢ r = 0 ∨ m = 0

Tactic:
algebra_compatible_smul S,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing T
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
r : R
m : T
h : f r • m = 0
⊢ r = 0 ∨ m = 0
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case hg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (f.support.biUnion fun i ↦ (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

pp: case hfg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
· simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not,
      and_imp, forall_exists_index]
    simp +contextual

Goal state after:
case hfg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
i : I
hi : f i ≠ 0
⊢ (a i) j • f i = 0

Tactic:
rw [hj i hi, zero_smul]

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ P.primeCompl
⊢ ∃ s_1, IsUnit (f s_1) ∧ IsLocalization.mk' (Localization.AtPrime P) x ⟨s, hs⟩ * f s_1 ∈ f.range

Tactic:
exact ⟨algebraMap _ _ s, by simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp [f]⟩

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
⊢ x ∈ Submodule.span R ↑(Finset.image₂ (fun i j ↦ f i * b j) f.support f.support)

Tactic:
← mul_one x,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
⊢ x * 1 ∈ Submodule.span R ↑(Finset.image₂ (fun i j ↦ f i * b j) f.support f.support)
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) (maximalIdeal (Localization.AtPrime p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p

Tactic:
Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (Localization.localRingHom p q (algebraMap R S) ⋯) (maximalIdeal (Localization.AtPrime p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Countable R
inst✝ : Countable ι
v : ι → M
⊢ Countable ↥(Submodule.span R (Set.range v))

Tactic:
by
  refine Set.countable_coe_iff.mpr (Set.Countable.mono ?_ (Set.countable_range
      (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))
  exact fun _ h => Finsupp.mem_span_range_iff_exists_finsupp.mp (SetLike.mem_coe.mp h)

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Zero ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ One ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Add ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Sub ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Mul ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inv ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Div ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ LE ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Bot ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inhabited ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Nontrivial ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommSemiring ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ Algebra ℝ≥0 ℝ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ DistribMulAction ℝ≥0ˣ ℝ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ MonoidWithZero ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommMonoidWithZero ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommGroupWithZero ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrder ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ OrderBot ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ PartialOrder ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ AddCommMonoid ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ IsOrderedAddMonoid ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DistribLattice ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeInf ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeSup ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ Semiring ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ CommMonoid ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrderedCommMonoidWithZero ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DenselyOrdered ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ NoMaxOrder ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ OrderedSub ℝ≥0

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy
  all_goals simp_all

Goal state after: