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

Goal state before:
pp: case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
| fun j ↦ of (fun i j ↦ (trace A B) (b i * b j)) i j * b.equivFun z j

Tactic:
ext

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| of (fun i j ↦ (trace A B) (b i * b j)) i x✝ * b.equivFun z x✝
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
| fun x ↦ b.equivFun z x • (b i * b x)

Tactic:
ext

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| b.equivFun z x✝ • (b i * b x✝)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
⊢ ∑ x, ↑↑x = 0

Tactic:
have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x ∈ map a_mul_emb univ, ↑↑x = ∑ x, ↑↑(a_mul_emb x)
⊢ ∑ x, ↑↑x = 0
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
⊢ fixingSubgroup G ↑⊤ = ⊥

Tactic:
ext

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
x✝ : G
⊢ x✝ ∈ fixingSubgroup G ↑⊤ ↔ x✝ ∈ ⊥
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
hGKL : IsGaloisGroup G K L
⊢ FixedPoints.intermediateField ↥⊤ = FixedPoints.intermediateField G

Tactic:
ext

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
hGKL : IsGaloisGroup G K L
x✝ : L
⊢ x✝ ∈ FixedPoints.intermediateField ↥⊤ ↔ x✝ ∈ FixedPoints.intermediateField G
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ a = 1

Tactic:
ext

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := ⋯
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a = ↑↑1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := ⋯
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a = ↑↑1

Tactic:
rwa [← sub_eq_zero]

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁷ : Group G
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : MulSemiringAction G L
H : Subgroup G
hGKL : IsGaloisGroup G K L
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
⊢ ↑(FixedPoints.intermediateField ↥H) = Set.range ⇑(algebraMap B L)

Tactic:
ext

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁷ : Group G
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : MulSemiringAction G L
H : Subgroup G
hGKL : IsGaloisGroup G K L
B : Type u_5
inst✝² : CommSemiring B
inst✝¹ : Algebra B L
inst✝ : IsGaloisGroup (↥H) B L
x✝ : L
⊢ x✝ ∈ ↑(FixedPoints.intermediateField ↥H) ↔ x✝ ∈ Set.range ⇑(algebraMap B L)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ∀ (x : Fin pb.dim), ¬(x ∈ Finset.univ ∧ ∃ a ∈ Finset.Ioi x, (e a) pb.gen = (e x) pb.gen)

Tactic:
rintro i ⟨_, j, hij, h⟩

Goal state after:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
i : Fin pb.dim
left✝ : i ∈ Finset.univ
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h : (e j) pb.gen = (e i) pb.gen
⊢ False
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val

Tactic:
simp_rw [← mul_pow]

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ (↑↑x * ↑↑a) ^ k) univ.val
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
⊢ traceForm K L = 0

Tactic:
ext

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
x✝ y✝ : L
⊢ ((traceForm K L) x✝) y✝ = (0 x✝) y✝
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
h : ↑↑a ^ k - 1 = 0
⊢ a ^ k = 1

Tactic:
ext

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
h : ↑↑a ^ k - 1 = 0
⊢ ↑↑(a ^ k) = ↑↑1
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
⊢ ⇑pb.basis.traceDual = fun i ↦ (minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))

Tactic:
Basis.traceDual_eq_iff

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
⊢ ∀ (i j : Fin pb.dim),
    ((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j) =
      if j = i then 1 else 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: 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

Tactic:
constructor

Goal state after:
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

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: a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b

Tactic:
constructor

Goal state after:
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b

case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ EuclideanDomain.gcd a b

Tactic:
exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

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

Goal state before:
pp: case intro
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✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ ¬(algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a)) = 0

Tactic:
algebraMap_eq_zero_iff,

Goal state after:
case intro
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✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ ¬(algebraMap B (B ⧸ Q)) ((algebraMap A B) a) = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
fin_cases x

Goal state after:
case inl.«0»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i ↦ i) ⟨0, ⋯⟩

case inl.«1»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i ↦ i) ⟨1, ⋯⟩
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
f : Gal(L/K)
x : L
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
⊢ f x = x

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x

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
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
⊢ f ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) = (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
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
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ ¬(algebraMap K L) ((algebraMap (A ⧸ P) K) a) = 0

Tactic:
algebraMap_eq_zero_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
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ ¬(algebraMap (A ⧸ P) K) a = 0
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
⊢ RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}

Tactic:
ext

Goal state after:
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
⊢ f = g

Tactic:
have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
  rw [Subtype.coe_mk] at this
  rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]

Goal state after:
Module: Mathlib.Data.ZMod.QuotientRing

Goal state before:
pp: n : ℕ
⊢ (↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})

Tactic:
ext

Goal state after:
n : ℕ
x✝ : ℤ
⊢ ((↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n))) x✝ = (Ideal.Quotient.mk (Ideal.span {↑n})) x✝
Module: Mathlib.Data.ZMod.QuotientRing

Goal state before:
pp: n : ℤ
⊢ (↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})

Tactic:
ext

Goal state after:
n x✝ : ℤ
⊢ ((↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs))) x✝ = (Ideal.Quotient.mk (Ideal.span {n})) x✝
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
⊢ Function.Surjective ⇑(stabilizerHom G P Q K L)

Tactic:
let _ := MulSemiringAction.compHom L (stabilizerHom G P Q K L)
  intro f
  obtain ⟨g, hg⟩ := FixedPoints.toAlgAut_surjective (MulAction.stabilizer G Q) L
    (AlgEquiv.ofRingEquiv (f := f) (fun x ↦ fixed_of_fixed2 G P Q K L f x x.2))
  exact ⟨g, by rwa [AlgEquiv.ext_iff] at hg ⊢⟩

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x) ↔ ∀ (i : ι), a i ∣ (b'.repr x) i

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
⊢ (∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x) → ∀ (i : ι), a i ∣ (b'.repr x) i

case mpr
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
⊢ (∀ (i : ι), a i ∣ (b'.repr x) i) → ∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
x : ι → R
⊢ (∃ y, (∀ (i : ι), a i ∣ (b'.repr y) i) ∧ ⇑(b'.repr y) = x) ↔ ∀ (i : ι), ∃ a_1, x i = a i * a_1

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := ⋯
x : ι → R
⊢ (∃ y, (∀ (i : ι), a i ∣ (b'.repr y) i) ∧ ⇑(b'.repr y) = x) → ∀ (i : ι), ∃ a_2, x i = a i * a_2

case mpr
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this : Fintype ι
a : ι → R := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := ⋯
x : ι → R
⊢ (∀ (i : ι), ∃ a_1, x i = a i * a_1) → ∃ y, (∀ (i : ι), a i ∣ (b'.repr y) i) ∧ ⇑(b'.repr y) = x