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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ : sf
⊢ ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ : sf
⊢ ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M✝¹ : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M✝¹
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M✝¹
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M✝¹
inst✝ : Module.Invertible R N
M✝ : (Skeleton (SemimoduleCat R))ˣ
M : Skeleton (SemimoduleCat R)
⊢ ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out M)

Tactic:
;

Goal state after:
R : Type u
M✝¹ : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M✝¹
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M✝¹
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M✝¹
inst✝ : Module.Invertible R N
M✝ : (Skeleton (SemimoduleCat R))ˣ
M : Skeleton (SemimoduleCat R)
⊢ ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out M)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x✝ : Pic R
⊢ ((mapAlgebra A B).comp (mapAlgebra R A)) x✝ = (mapAlgebra R B) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x✝ : Pic R
⊢ ((mapAlgebra A B).comp (mapAlgebra R A)) x✝ = (mapAlgebra R B) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : Pic R
⊢ (mapAlgebra R R) x✝ = (MonoidHom.id (Pic R)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : Pic R
⊢ (mapAlgebra R R) x✝ = (MonoidHom.id (Pic R)) x✝
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧ ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → s ⊆ s_1 → s = s_1) ↔
    AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ⊆ y → s = y

Tactic:
;

Goal state after:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧ ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → s ⊆ s_1 → s = s_1) ↔
    AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ⊆ y → s = y
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝² : P.IsMaximal
x✝¹ x✝ : M
⊢ ((AlgebraTensorModule.curry ((IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(TensorProduct.comm R M M) ∘ₗ ff P))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) ∘ₗ ff P))
        x✝¹)
      x✝

Tactic:
;

Goal state after:
case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝² : P.IsMaximal
x✝¹ x✝ : M
⊢ ((AlgebraTensorModule.curry ((IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(TensorProduct.comm R M M) ∘ₗ ff P))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) ∘ₗ ff P))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
i : ↥S
x : A
hx : x ∈ ↑I
⊢ (LinearMap.mulRight R (r ↑i • a i)) x ∈ ↑I * ↑I⁻¹

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
i : ↥S
x : A
hx : x ∈ ↑I
⊢ (LinearMap.mulRight R (r ↑i • a i)) x ∈ ↑I * ↑I⁻¹
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard

Tactic:
;

Goal state after:
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
⊢ ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
hB₁ : M.IsBase B₁
h : B₁.Finite
⊢ B.Finite

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
hB₁ : M.IsBase B₁
h : B₁.Finite
⊢ B.Finite
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ M.RankPos

Tactic:
rankPos_iff

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ ¬M.IsBase ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = x • β - y • β

Tactic:
;

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = x • β - y • β
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
x✝² : A
x✝¹ : ↥↑I
x✝ : ↥S
⊢ ((AlgebraTensorModule.curry (↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f)) x✝²) x✝¹ x✝ =
    ((AlgebraTensorModule.curry ((LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m)) x✝²) x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
x✝² : A
x✝¹ : ↥↑I
x✝ : ↥S
⊢ ((AlgebraTensorModule.curry (↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f)) x✝²) x✝¹ x✝ =
    ((AlgebraTensorModule.curry ((LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m)) x✝²) x✝¹ x✝
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
x✝¹ : A
x✝ : ↥↑I
⊢ ((AlgebraTensorModule.curry m) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (⊤.mulMap ↑I ∘ₗ ↑(LinearEquiv.rTensor (↥↑I) topEquiv.symm))) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
x✝¹ : A
x✝ : ↥↑I
⊢ ((AlgebraTensorModule.curry m) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (⊤.mulMap ↑I ∘ₗ ↑(LinearEquiv.rTensor (↥↑I) topEquiv.symm))) x✝¹) x✝
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r : F[X]
hm : 0 < m
h : α ^ m * (aeval (α ^ n)) 0 - (aeval (α ^ n)) r = 0
hzero : ¬(aeval (α ^ n)) 0 = 0
⊢ False

Tactic:
;

Goal state after:
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r : F[X]
hm : 0 < m
h : α ^ m * (aeval (α ^ n)) 0 - (aeval (α ^ n)) r = 0
hzero : ¬(aeval (α ^ n)) 0 = 0
⊢ False
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
he : f ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {f})
hf : f ∈ B' \ (B \ {f})
hfB : M.Indep (insert f (B \ {f}))
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
he : f ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {f})
hf : f ∈ B' \ (B \ {f})
hfB : M.Indep (insert f (B \ {f}))
⊢ False
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ (↑(I * J)).subtype ∘ₗ (↑I).mulMap' ↑J =
    (LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑J).subtype) ∘ₗ LinearMap.rTensor (↥↑J) (↑I).subtype

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ (↑(I * J)).subtype ∘ₗ (↑I).mulMap' ↑J =
    (LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑J).subtype) ∘ₗ LinearMap.rTensor (↥↑J) (↑I).subtype
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
x✝¹ : ↥↑I
x✝ : ↥↑J
⊢ ((AlgebraTensorModule.curry ((↑(I * J)).subtype ∘ₗ (↑I).mulMap' ↑J)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ((LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑J).subtype) ∘ₗ LinearMap.rTensor (↥↑J) (↑I).subtype))
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
x✝¹ : ↥↑I
x✝ : ↥↑J
⊢ ((AlgebraTensorModule.curry ((↑(I * J)).subtype ∘ₗ (↑I).mulMap' ↑J)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ((LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑J).subtype) ∘ₗ LinearMap.rTensor (↥↑J) (↑I).subtype))
        x✝¹)
      x✝
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ False

Tactic:
refine hB.not_prop_of_ssuperset ?_ hind

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert x (insert f (B \ {x}))
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Nonempty (↥↑(I * J) ≃ₗ[R] ↥↑I ⊗[R] ↥↑J)

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I✝ J✝ I J : (Submodule R A)ˣ
⊢ Nonempty (↥↑(I * J) ≃ₗ[R] ↥↑I ⊗[R] ↥↑J)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ I ∈ (unitsToPic R A).ker ↔ I ∈ (Units.map ↑(spanSingleton R)).range

Tactic:
;

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
⊢ I ∈ (unitsToPic R A).ker ↔ I ∈ (Units.map ↑(spanSingleton R)).range
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M₁ : Matroid α
⊢ M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)

Tactic:
;

Goal state after:
α : Type u_1
M₁ : Matroid α
⊢ M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f = Polynomial.map ((algebraMap (↥K) E).comp (algebraMap F ↥K)) (minpoly F α)

Tactic:
;

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f = Polynomial.map ((algebraMap (↥K) E).comp (algebraMap F ↥K)) (minpoly F α)