awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
have hc : ∀ (a : A),
  Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
Tactic: have hc (a : A) : (algebraMap K L) (algebraMap A K a) = (algebraMap B L) (algebraMap A B a) := by
    simp_rw [← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
have this : Algebra.IsIntegral A B
Tactic: have := hAB.isIntegral A B G
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this : Algebra.IsIntegral A B
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
have this₁ : Nontrivial A
Tactic: have : Nontrivial A := (IsFractionRing.nontrivial_iff_nontrivial A K).mpr inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this : Nontrivial A
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
have this₁ : Nontrivial B
Tactic: have : Nontrivial B := (IsFractionRing.nontrivial_iff_nontrivial B L).mpr inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
have obtain : ∀ (x y : B) (hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y)
  (h :
    ∀ (g : G),
      g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)),
  ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
Tactic: have hy' : algebraMap B L y ≠ 0 := by simpa using nonZeroDivisors.ne_zero hy
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have obtain : ∀ (b : B) (a : A) (ha : a ≠ 0) (hb : a • x = y * b),
  ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: obtain ⟨b, a, ha, hb⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A) y).exists_smul_eq_mul x hy
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
ha : a ≠ 0
hb : a • x = y * b
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have hb₁ : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
Tactic: rw [mul_comm, Algebra.smul_def, mul_comm] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
ha : a ≠ 0
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have ha₁ : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
Tactic: replace ha : (algebraMap B L) (algebraMap A B a) ≠ 0 := by simpa [← hc]
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
have rw : HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) =
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
rw :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
have rw₁ : (algebraMap B L : (a : B) → L) (HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
rw :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₁ :
  (algebraMap B L : (a : B) → L) (HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
have rw₂ : (algebraMap B L : (a : B) → L) (b * y) =
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
rw :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₁ :
  (algebraMap B L : (a : B) → L) (HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₂ :
  (algebraMap B L : (a : B) → L) (b * y) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
have rw₃ : HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L) =
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
Tactic: rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
have hxy : HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
Tactic: have hxy : algebraMap B L x / algebraMap B L y =
    algebraMap B L b / algebraMap B L (algebraMap A B a) := by
    rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]