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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R M) *
        (equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R N))

Tactic:
[

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R M) *
        (equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R N))
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h✝ : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
φ : ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L := ⋯.some
φ' : ↥(normalClosure F K L') →ₐ[F] L := φ.comp (inclusion ⋯)
x✝¹ x✝ : K →ₐ[F] L'
h : (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝¹ = (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝
⊢ (normalClosure.algHomEquiv F K L').symm x✝¹ = (normalClosure.algHomEquiv F K L').symm x✝

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h✝ : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
φ : ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L := ⋯.some
φ' : ↥(normalClosure F K L') →ₐ[F] L := φ.comp (inclusion ⋯)
x✝¹ x✝ : K →ₐ[F] L'
h :
  ⇑((φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝¹) =
    ⇑((φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝)
⊢ ⇑((normalClosure.algHomEquiv F K L').symm x✝¹) = ⇑((normalClosure.algHomEquiv F K L').symm x✝)
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L

Tactic:
[

Goal state after:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L
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
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk R (x✝¹.AsModule ⊗[R] x✝.AsModule) = 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✝⁴ : Module.Invertible R M
inst✝³ : Module.Invertible R N
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk R (x✝¹.AsModule ⊗[R] x✝.AsModule) = x✝¹ * x✝
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:
rw [MonoidHom.comp_apply, mapAlgebra_mapAlgebra]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
[

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f

Tactic:
[

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f
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, ⋯⟩
x : ↥↑I
⊢ ↑(∑ d, f x d • ⟨b d, ⋯⟩) = ↑(LinearMap.id 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, ⋯⟩
x : ↥↑I
⊢ ↑(∑ d, f x d • ⟨b d, ⋯⟩) = ↑(LinearMap.id x)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ {I | M.Indep I} = ↑(lowerClosure {B | M.IsBase B})

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
⊢ {I | M.Indep I} = ↑(lowerClosure {B | M.IsBase B})
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
[

Goal state after:
case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (insert f (B \ {e}))
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.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
h' : M₁.Indep = M₂.Indep
B : Set α
x✝ : B ⊆ M₁.E
⊢ M₁.IsBase B ↔ M₂.IsBase B

Tactic:
[

Goal state after:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
h' : M₁.Indep = M₂.Indep
B : Set α
x✝ : B ⊆ M₁.E
⊢ M₁.IsBase B ↔ M₂.IsBase B
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α_1⟯ = IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯

Tactic:
[

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α_1⟯ = IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x✝ : Set α
⊢ Indep x✝ ↔ ∃ B, IsBase B ∧ x✝ ⊆ B

Tactic:
[

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x✝ : Set α
⊢ Indep x✝ ↔ ∃ B, IsBase B ∧ x✝ ⊆ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ B, IsBase B

Tactic:
[

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ B, IsBase B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ExchangeProperty IsBase

Tactic:
[

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ExchangeProperty IsBase
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
[

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ E

Tactic:
[

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ E
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
by
  rw [IsBasis, maximal_subset_iff]
  tauto

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
⊢ F⟮α⟯ = ⊤ ↔ Function.Injective fun φ ↦ φ α

Tactic:
[

Goal state after:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
⊢ F⟮α⟯ = ⊤ ↔ Function.Injective fun φ ↦ φ α
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis' J X ∧ I ⊆ J

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis' J X ∧ I ⊆ J
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis J (X ∩ M.E) ∧ I ⊆ J

Tactic:
exact hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I
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
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ ⇑(I * submoduleAlgebra e).subtype ∘ ⇑(I.mulMap' (submoduleAlgebra e)) =
    ⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘
      ⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) 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
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
I : Submodule R A
⊢ ⇑(I * submoduleAlgebra e).subtype ∘ ⇑(I.mulMap' (submoduleAlgebra e)) =
    ⇑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘
      ⇑(LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ Pic.mk R (M.AsModule ⊗[R] M⁻¹.AsModule) = 1

Tactic:
[

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ Pic.mk R (M.AsModule ⊗[R] M⁻¹.AsModule) = 1
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case h
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert e I) B

Tactic:
[

Goal state after:
case h
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert e I) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
⊢ M.IsBasis (insert e I) (insert e X)

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
⊢ M.IsBasis (insert e I) (insert e X)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBasis B X

Tactic:
isBasis_iff,

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.Indep B ∧ B ⊆ X ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1)
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)

Tactic:
this

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1)
⊢ IsUnit
    (R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1))
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    ⊤ *
      (R ∙
        ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
                tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
            1))
⊢ IsUnit
    (R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1))

Tactic:
[

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    ⊤ *
      (R ∙
        ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
                tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
            1))
⊢ IsUnit
    (R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1))
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (K ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint K B) ∧ K ⊆ X) J

Tactic:
[

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (K ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint K B) ∧ K ⊆ X) J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ (M ↾ X).IsBase I ↔ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M = freeOn M.E

Tactic:
by
  simp [eq_freeOn_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Tactic:
[

Goal state after:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x