awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
calc_1 :
  ∀ (u : Rˣ) (hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u),
    card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} = c
calc_2 : Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0

Tactic:
calc
      ∑ g : G, f g = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) :=
        sum_comp ((↑) : Rˣ → R) f.toHomUnits
      _ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
        (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
      _ = ∑ b : MonoidHom.range f.toHomUnits, c • (b.1 : R) :=
        (Finset.sum_subtype _ (by simp) _)
      _ = c • ∑ b : MonoidHom.range f.toHomUnits, (b.1 : R) := smul_sum.symm
      _ = c • 0 := congr_arg₂ _ rfl ?_
      -- remaining goal 2, proven below
      _ = 0 := smul_zero _

Premises used: Units.val, MonoidHom.range, Finset.univ, MonoidHom.toHomUnits, smul_zero, Finset.sum_subtype, Finset.sum_comp, Finset.smul_sum, Eq.symm, DFunLike.coe, Finset.image, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
u : Rˣ
hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u
calc_1 : Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) u
calc_1₁ : Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) 1
⊢ card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} = c

Tactic:
apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits

Premises used: MonoidHom.toHomUnits, MonoidHom.card_fiber_eq_of_mem_range
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
u : Rˣ
hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u
⊢ Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) u

Tactic:
simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu

Premises used: Finset.mem_univ, Set.mem_range, Finset.mem_image, true_and
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
u : Rˣ
hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u
⊢ Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) 1

Tactic:
⟨1, f.toHomUnits.map_one⟩

Premises used: Set.Mem, setOf, MonoidHom.toHomUnits, MonoidHom.map_one, Exists.intro, Set.range, OfNat.ofNat
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
u : Rˣ
hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u
⊢ Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) 1

Tactic:
exact ⟨1, f.toHomUnits.map_one⟩
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ ∀ a ∈ range (orderOf x), Membership.mem (γ := Finset ↥f.toHomUnits.range) univ ((fun (x_1 : ℕ) ↦ x ^ x_1) a)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Set.InjOn.{0, u_1} (β := ↥f.toHomUnits.range) (fun (x_1 : ℕ) ↦ x ^ x_1) (↑(range (orderOf x)) : Set ℕ)

Tactic:
simpa using pow_injOn_Iio_orderOf

Premises used: pow_injOn_Iio_orderOf
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
b : ↥f.toHomUnits.range
h : b ∈ (↑univ : Set ↥f.toHomUnits.range)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = b
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) (n % orderOf x) = b

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ ∀ a ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ a = (↑(↑((fun (x_1 : ℕ) ↦ x ^ x_1) a) : Rˣ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0

Tactic:
?_
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
calc_2 : Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 0

Tactic:
calc
      (∑ b : MonoidHom.range f.toHomUnits, (b.1 : R))
        = ∑ n ∈ range (orderOf x), (x.1 : R) ^ n :=
        Eq.symm <|
          sum_nbij (x ^ ·) (by simp)
            (by simpa using pow_injOn_Iio_orderOf)
            (fun b _ => let ⟨n, hn⟩ := hx b
              ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)), by simp [hn]⟩)
            (by simp)
      _ = 0 := ?_

Premises used: Iff.mpr, Units.val, Finset.univ, Finset.sum_nbij, Membership.mem, _private.0.sum_hom_units_eq_zero.match_5, Finset.mem_range, Nat.mod_lt, Finset.range, orderOf, HMod.hMod, SetLike.coe, HPow.hPow, And.intro, Exists.intro, Set.image, Eq.symm, Subtype.val, orderOf_pos, Finset.sum
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
calc_2 : (↑(↑x : Rˣ) : R) ^ orderOf x - 1 = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0

Tactic:
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]

Premises used: MulZeroClass.zero_mul, geom_sum_mul, mul_left_inj'
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
calc_2 : (↑(↑(x ^ orderOf x) : Rˣ) : R) - 1 = 0
⊢ (↑(↑x : Rˣ) : R) ^ orderOf x - 1 = 0

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ (↑(↑(x ^ orderOf x) : Rˣ) : R) - 1 = 0

Tactic:
simp [pow_orderOf_eq_one]

Premises used: pow_orderOf_eq_one
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
inst_4 : Decidable (f = 1)
pos : ∀ (h : f = 1), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(Fintype.card G) : R)
neg : ∀ (h : ¬f = 1), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑0 : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(if f = 1 then Fintype.card G else 0) : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
inst_4 : Decidable (f = 1)
h : f = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(Fintype.card G) : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
inst_4 : Decidable (f = 1)
h : ¬f = 1
neg : Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑0 : R)

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
inst_4 : Decidable (f = 1)
h : ¬f = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0

Tactic:
sum_hom_units_eq_zero f h

Premises used: sum_hom_units_eq_zero
-- Module: Mathlib.RingTheory.IntegralDomain
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
inst_4 : Decidable (f = 1)
h : ¬f = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0

Tactic:
exact sum_hom_units_eq_zero f h

Premises used: sum_hom_units_eq_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsAlgebraic K L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
g : Gal(L/K)
b : B
l : L
simp :
  HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b) ∨ g • l = 0
⊢ g • b • l = (g • b) • g • l

Tactic:
simp only [Algebra.smul_def, smul_mul', mul_eq_mul_right_iff]

Premises used: mul_eq_mul_right_iff, Algebra.smul_def, smul_mul'
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsAlgebraic K L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
g : Gal(L/K)
b : B
l : L
⊢ HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b) ∨ g • l = 0

Tactic:
Or.inl (algebraMap_galRestrictHom_apply A K L B g b).symm

Premises used: AlgEquiv.toAlgHom, Or.inl, Eq.symm, algebraMap_galRestrictHom_apply
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsAlgebraic K L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
g : Gal(L/K)
b : B
l : L
⊢ HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b) ∨ g • l = 0

Tactic:
exact Or.inl (algebraMap_galRestrictHom_apply A K L B g b).symm

Premises used: AlgEquiv.toAlgHom, Or.inl, Eq.symm, algebraMap_galRestrictHom_apply
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h : IsGalois K L
⊢ Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥

Tactic:
replace h := ((IsGalois.tfae (F := K) (E := L)).out 0 1).mp h
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
⊢ IsInvariant.{u_1, u_4, u_3} A B Gal(L/K)

Tactic:
⟨fun b hb ↦ ?_⟩

Premises used: Algebra.IsInvariant.mk
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
refine : ∀ (b : B) (hb : ∀ (g : Gal(L/K)), g • b = b), ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
⊢ IsInvariant.{u_1, u_4, u_3} A B Gal(L/K)

Tactic:
refine ⟨fun b hb ↦ ?_⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : ∀ (g : Gal(L/K)), g • b = b
g : Gal(L/K)
property : Membership.mem (γ := Subgroup Gal(L/K)) ⊤ g
⊢ HSMul.hSMul (β := L) (Subtype.mk (p := fun (x : Gal(L/K)) ↦ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ x) g property)
      ((algebraMap B L : (a : B) → L) b : L) =
    (algebraMap B L : (a : B) → L) b

Tactic:
(algebraMap_galRestrict_apply A g b).symm.trans (congrArg (algebraMap B L) (hb g))

Premises used: Algebra.algebraMap, congrArg, algebraMap_galRestrict_apply, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : ∀ (g : Gal(L/K)), g • b = b
g : Gal(L/K)
property : Membership.mem (γ := Subgroup Gal(L/K)) ⊤ g
⊢ HSMul.hSMul (β := L) (Subtype.mk (p := fun (x : Gal(L/K)) ↦ Membership.mem (γ := Subgroup Gal(L/K)) ⊤ x) g property)
      ((algebraMap B L : (a : B) → L) b : L) =
    (algebraMap B L : (a : B) → L) b

Tactic:
exact (algebraMap_galRestrict_apply A g b).symm.trans (congrArg (algebraMap B L) (hb g))

Premises used: Algebra.algebraMap, congrArg, algebraMap_galRestrict_apply, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : ∀ (g : Gal(L/K)), g • b = b
⊢ Membership.mem.{u_3, u_3} (α := L) (γ := IntermediateField K L) (IntermediateField.fixedField ⊤)
    ((algebraMap B L : (a : B) → L) b : L)

Tactic:
replace hb : algebraMap B L b ∈ IntermediateField.fixedField (⊤ : Subgroup Gal(L/K)) := by
    rintro ⟨g, -⟩
    exact (algebraMap_galRestrict_apply A g b).symm.trans (congrArg (algebraMap B L) (hb g))
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb :
  Membership.mem.{u_3, u_3} (α := L) (γ := IntermediateField K L) (IntermediateField.fixedField ⊤)
    ((algebraMap B L : (a : B) → L) b : L)
⊢ Membership.mem.{u_3, u_3} (α := L) (γ := Set L) (Set.range.{u_3, u_2 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
    ((algebraMap B L : (a : B) → L) b : L)

Tactic:
rw [h, IntermediateField.mem_bot] at hb

Premises used: IntermediateField.mem_bot
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb :
  Membership.mem.{u_3, u_3} (α := L) (γ := Set L) (Set.range.{u_3, u_2 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
    ((algebraMap B L : (a : B) → L) b : L)
obtain :
  ∀ (k : K) (hk : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) k : L) ((algebraMap B L : (a : B) → L) b : L)),
    ∃ (a : A), (algebraMap A B : (a : A) → B) a = b
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = b

Tactic:
obtain ⟨k, hk⟩ := hb
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : FiniteDimensional K L
h_1 : IsGalois K L
h : Eq.{u_3 + 1} (α := IntermediateField K L) (IntermediateField.fixedField ⊤) ⊥
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : Eq.{u_3 + 1} (α := L) ((algebraMap K L : (a : K) → L) k : L) ((algebraMap B L : (a : B) → L) b : L)
⊢ IsIntegral A b

Tactic:
have hb : IsIntegral A b := IsIntegralClosure.isIntegral A L b