awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
f : S →+* R
s : S
x : A
⊢ s • x = HSMul.hSMul.{u, w, w} (α := R) ((f : (a : S) → R) s : R) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
f : S →+* R
⊢ Eq (α := S →+* A) (algebraMap S A) (RingHom.comp (algebraMap R A) f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
f : S →+* R
s : S
⊢ Eq.{w + 1} (α := A) ((algebraMap S A : (a : S) → A) s : A)
    ((algebraMap R A : (a : R) → A) ((f : (a : S) → R) s : R) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x y : R
⊢ OneHom.toFun (↑(↑(algebraMap R A) : R →* A) : OneHom R A) (x • y) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (OneHom.toFun (↑(↑(algebraMap R A) : R →* A) : OneHom R A) y)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{w + 1} (α := A) ((Algebra.linearMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : R) → A) (⇑(Algebra.linearMap R A) : (a : R) → A) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₗ[R] R) (Algebra.linearMap R R) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →+* R) (algebraMap R R) (RingHom.id R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
inst : CommSemiring R
x : R
⊢ (algebraMap R R : (a : R) → R) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
inst : CommSemiring R
x y : R
⊢ x • y = x * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst : SMul A B
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra B C
inst_4 : SMul A C
inst_5 : IsScalarTower A B C
⊢ (↑(a • b) : C) = HSMul.hSMul (β := C) a (↑b : C)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst : SMul A B
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra B C
inst_4 : Monoid A
inst_5 : MulDistribMulAction A C
inst_6 : SMulDistribClass A B C
⊢ (↑(a • b) : C) = HSMul.hSMul (β := C) a (↑b : C)

Tactic:
simp [Algebra.algebraMap_eq_smul_one, smul_distrib_smul]

Premises used: Algebra.algebraMap_eq_smul_one, SMulDistribClass.smul_distrib_smul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst : SMul A B
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra B C
inst_4 : SMul A C
inst_5 : IsScalarTower A B C
⊢ (algebraMap B C : (a : B) → C) (a • b) = HSMul.hSMul (β := C) a ((algebraMap B C : (a : B) → C) b : C)

Tactic:
coe_smul _ _ _

Premises used: algebraMap.coe_smul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
A : Type u_1
B : Type u_2
a : A
b : B
C : Type u_3
inst : SMul A B
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra B C
inst_4 : Monoid A
inst_5 : MulDistribMulAction A C
inst_6 : SMulDistribClass A B C
⊢ (algebraMap B C : (a : B) → C) (a • b) = HSMul.hSMul (β := C) a ((algebraMap B C : (a : B) → C) b : C)

Tactic:
coe_smul' _ _ _

Premises used: algebraMap.coe_smul'
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Algebra.IsEpi R A
a : A
⊢ Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (1 ⊗ₜ[R] a) : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
refine :
  ∀ (h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)) (x y : A ⊗[R] A)
    (hxy :
      Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
        ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)),
    x = y
⊢ Algebra.IsEpi R A ↔ ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)

Tactic:
refine ⟨fun h a ↦ IsEpi.injective_lift_mul <| by simp, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
⊢ Eq.{u_2 + 1} (α := A ⊗[R] A) 0 (0 ⊗ₜ[R] 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
⊢ ∃ (a : A), Eq (α := A ⊗[R] A) 0 (a ⊗ₜ[R] 1)

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
h₁ : Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)
⊢ ∃ (a : A), Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) (a ⊗ₜ[R] 1)

Tactic:
use u * v
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ u ⊗ₜ[R] v = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
rw rw₁ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
⊢ HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = (u * v) ⊗ₜ[R] 1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
calc : u ⊗ₜ[R] v = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v)
calc₁ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (1 ⊗ₜ[R] v) = HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1)
calc₂ : HMul.hMul (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = (u * v) ⊗ₜ[R] 1
⊢ Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) ((u * v) ⊗ₜ[R] 1)

Tactic:
calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp

Premises used: HMul.hMul
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A ⊗[R] A
hu : ∃ (a : A), u = a ⊗ₜ[R] 1
hv : ∃ (a : A), v = a ⊗ₜ[R] 1
add : ∀ (u : A), ∃ (a : A), u ⊗ₜ[R] 1 + v = a ⊗ₜ[R] 1
⊢ ∃ (a : A), u + v = a ⊗ₜ[R] 1

Tactic:
obtain ⟨u, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ HAdd.hAdd (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = (u + v) ⊗ₜ[R] 1

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
u v : A
⊢ ∃ (a : A), HAdd.hAdd (α := A ⊗[R] A) (u ⊗ₜ[R] 1) (v ⊗ₜ[R] 1) = a ⊗ₜ[R] 1

Tactic:
exact ⟨u  + v, by simp [add_tmul]⟩
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x_1 y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x_1 : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
x : A ⊗[R] A
zero : ∃ (a : A), Eq (α := A ⊗[R] A) 0 (a ⊗ₜ[R] 1)
tmul : ∀ (u v : A), ∃ (a : A), Eq (α := A ⊗[R] A) (u ⊗ₜ[R] v) (a ⊗ₜ[R] 1)
add : ∀ (u v : A ⊗[R] A) (hu : ∃ (a : A), u = a ⊗ₜ[R] 1) (hv : ∃ (a : A), v = a ⊗ₜ[R] 1), ∃ (a : A), u + v = a ⊗ₜ[R] 1
⊢ ∃ (a : A), x = a ⊗ₜ[R] 1

Tactic:
induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩

Premises used: TensorProduct.tmul, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
⊢ ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1

Tactic:
have h' (x : A ⊗[R] A) : ∃ a : A, x = a ⊗ₜ 1 := by
    induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
x y : A ⊗[R] A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) x : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
obtain :
  ∀ (a : A)
    (hxy :
      Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
        ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)),
    a ⊗ₜ[R] 1 = y
⊢ x = y

Tactic:
obtain ⟨a, rfl⟩ := h' x

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
y : A ⊗[R] A
h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
a : A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) y : A)
obtain :
  ∀ (b : A)
    (hxy :
      Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
        ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (b ⊗ₜ[R] 1) : A)),
    Eq (α := A ⊗[R] A) (a ⊗ₜ[R] 1) (b ⊗ₜ[R] 1)
⊢ a ⊗ₜ[R] 1 = y

Tactic:
obtain ⟨b, rfl⟩ := h' y

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
h' : ∀ (x : A ⊗[R] A), ∃ (a : A), x = a ⊗ₜ[R] 1
a b : A
hxy :
  Eq (α := A) ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (a ⊗ₜ[R] 1) : A)
    ((lift (LinearMap.mul R A) : (a : A ⊗[R] A) → A) (b ⊗ₜ[R] 1) : A)
⊢ Eq (α := A ⊗[R] A) (a ⊗ₜ[R] 1) (b ⊗ₜ[R] 1)

Tactic:
aesop
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Algebra.IsEpi R A

Tactic:
(isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_

Premises used: Iff.mpr, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
refine : ∀ (a : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)
⊢ Algebra.IsEpi R A

Tactic:
refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_

Premises used: Iff.mpr, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
obtain :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A ⊗[R] A) (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) r : A ⊗[R] A)
      ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] A)
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] a) (a ⊗ₜ[R] 1)

Tactic:
obtain ⟨r, rfl⟩ := h a

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : R
rw : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1) (HSMul.hSMul (β := A) r 1 ⊗ₜ[R] 1)
rw₁ rw₂ : Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1) (1 ⊗ₜ[R] HSMul.hSMul (β := A) r 1)
⊢ Eq.{u_2 + 1} (α := A ⊗[R] A) (1 ⊗ₜ[R] (algebraMap R A : (a : R) → A) r : A ⊗[R] A)
    ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] A)

Tactic:
rw [algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
⊢ Algebra.IsEpi R A

Tactic:
(isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_

Premises used: Iff.mpr, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
refine : ∀ (x : A), Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1)
⊢ Algebra.IsEpi R A

Tactic:
refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_

Premises used: Iff.mpr, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
x : A
obtain :
  ∀ (a b : R) (hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b),
    Eq (α := A ⊗[R] A)
      (1 ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A))
      (HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A) ⊗ₜ[R]
        1)
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] x) (x ⊗ₜ[R] 1)

Tactic:
obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective R x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
set :
  let f : R →+* A := algebraMap R A;
  ∀ (hf : f = algebraMap R A),
    Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
      (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R] 1)
⊢ Eq (α := A ⊗[R] A)
    (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((algebraMap R A : (a : R) → A) a : A) ((algebraMap R A : (a : R) → A) b : A) ⊗ₜ[R] 1)

Tactic:
set f := algebraMap R A with hf

Premises used: Algebra.algebraMap
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
⊢ Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)

Tactic:
aesop
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
⊢ Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)

Tactic:
replace hb : f b ≠ 0 := by aesop
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
rw :
  Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
rw₁ rw₂ :
  Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] HDiv.hDiv (β := A) (HSMul.hSMul (β := A) a 1) ((f : (a : R) → A) b : A))
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A))
    (1 ⊗ₜ[R] (a • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))

Tactic:
rw [← smul_div_assoc, algebraMap_eq_smul_one a]

Premises used: Algebra.algebraMap_eq_smul_one, smul_div_assoc
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
rw :
  Eq (α := A ⊗[R] A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
rw₁ rw₂ :
  Eq (α := A ⊗[R] A) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
    (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
⊢ Eq (α := A ⊗[R] A) (1 ⊗ₜ[R] (a • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)) : A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)

Tactic:
rw [← smul_tmul, algebraMap_eq_smul_one a]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
rw :
  Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) b : A)
          (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)
rw₁ rw₂ :
  Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
⊢ Eq (α := A ⊗[R] A)
    ((f : (a : R) → A) a ⊗ₜ[R] HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) : A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
        HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A) :
      A ⊗[R] A)

Tactic:
rw [smul_def, mul_div_cancel₀ _ hb]

Premises used: mul_div_cancel₀, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Field A
inst_3 : Algebra R A
inst_4 : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : Ne.{u_2 + 1} (α := A) ((f : (a : R) → A) b : A) (0 : A)
rw rw₁ :
  Eq (α := A ⊗[R] A)
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))
⊢ Eq (α := A ⊗[R] A)
    ((b • HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A)) ⊗ₜ[R]
      HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A))
    (HDiv.hDiv (α := A) (β := A) ((f : (a : R) → A) a : A) ((f : (a : R) → A) b : A) ⊗ₜ[R]
      (b • HDiv.hDiv (α := A) (β := A) (1 : A) ((f : (a : R) → A) b : A)))

Tactic:
rw [smul_tmul]

Premises used: TensorProduct.smul_tmul