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

Goal state before:
pp: 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)
⊢ TensorProduct.comm R M M = LinearEquiv.refl R (M ⊗[R] M)

Tactic:
refine LinearEquiv.toLinearMap_injective <| LinearMap.eq_of_localization_maximal _ ff _ ff _ _
    fun P _ ↦ .trans (b := (TensorProduct.comm ..).toLinearMap) ?_ ?_

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
⊢ (IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(TensorProduct.comm R M M) =
    ↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M))

case refine_2
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
⊢ ↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) =
    (IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(LinearEquiv.refl R (M ⊗[R] M))
Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Goal state before:
pp: case hC
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
x✝ : F
⊢ (((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))).comp C) x✝ = ((↑(aeval x)).comp C) x✝

pp: case hX
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
i✝ : ι
⊢ ((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))) (X i✝) = ↑(aeval x) (X i✝)

Tactic:
<;>

Goal state after:
case hC
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
x✝ : F
⊢ (((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))).comp C) x✝ = ((↑(aeval x)).comp C) x✝

case hX
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
i✝ : ι
⊢ ((↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F)))) (X i✝) = ↑(aeval x) (X i✝)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case false
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E E' : IntermediateField F K
inst✝¹ : Normal F ↥E
inst✝ : Normal F ↥E'
⊢ Normal F ↥(Bool.rec E' E false)

pp: case true
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E E' : IntermediateField F K
inst✝¹ : Normal F ↥E
inst✝ : Normal F ↥E'
⊢ Normal F ↥(Bool.rec E' E true)

Tactic:
<;>

Goal state after:
case false
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E E' : IntermediateField F K
inst✝¹ : Normal F ↥E
inst✝ : Normal F ↥E'
⊢ Normal F ↥(Bool.rec E' E false)

case true
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E E' : IntermediateField F K
inst✝¹ : Normal F ↥E
inst✝ : Normal F ↥E'
⊢ Normal F ↥(Bool.rec E' E true)
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:
exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)

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

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

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

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

Tactic:
<;>

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

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

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

Goal state before:
pp: case h.a
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 • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _

Goal state after:
case h.a
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⟮α + y • β⟯
⊢ {α, β} ⊆ ↑F⟮α + 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
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:
simp_rw [coe_sum, coe_smul, Algebra.smul_def, hf, mul_assoc, ← Finset.mul_sum,
      Algebra.smul_mul_assoc, eq, (Finset.sum_coe_sort ..).trans hr.2, mul_one, id_apply]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a.inl
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)
x✝ y : F
hneq : ¬x✝ = y
x : E
f : F → IntermediateField F E := fun x_1 ↦ F⟮x + x_1 • β⟯
heq : F⟮x + x✝ • β⟯ = F⟮x + y • β⟯
αxβ_in_K : x + x✝ • β ∈ F⟮x + x✝ • β⟯
αyβ_in_K : x + y • β ∈ F⟮x + x✝ • β⟯
β_in_K : β ∈ F⟮x + x✝ • β⟯
α_in_K : x ∈ F⟮x + x✝ • β⟯
⊢ x ∈ ↑F⟮x + x✝ • β⟯

pp: case h.a.inr
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)
x✝ y : F
hneq : ¬x✝ = y
x : E
f : F → IntermediateField F E := fun x_1 ↦ F⟮α + x_1 • x⟯
heq : F⟮α + x✝ • x⟯ = F⟮α + y • x⟯
αxβ_in_K : α + x✝ • x ∈ F⟮α + x✝ • x⟯
αyβ_in_K : α + y • x ∈ F⟮α + x✝ • x⟯
β_in_K : x ∈ F⟮α + x✝ • x⟯
α_in_K : α ∈ F⟮α + x✝ • x⟯
⊢ x ∈ ↑F⟮α + x✝ • x⟯

Tactic:
<;>

Goal state after:
case h.a.inl
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)
x✝ y : F
hneq : ¬x✝ = y
x : E
f : F → IntermediateField F E := fun x_1 ↦ F⟮x + x_1 • β⟯
heq : F⟮x + x✝ • β⟯ = F⟮x + y • β⟯
αxβ_in_K : x + x✝ • β ∈ F⟮x + x✝ • β⟯
αyβ_in_K : x + y • β ∈ F⟮x + x✝ • β⟯
β_in_K : β ∈ F⟮x + x✝ • β⟯
α_in_K : x ∈ F⟮x + x✝ • β⟯
⊢ x ∈ ↑F⟮x + x✝ • β⟯

case h.a.inr
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)
x✝ y : F
hneq : ¬x✝ = y
x : E
f : F → IntermediateField F E := fun x_1 ↦ F⟮α + x_1 • x⟯
heq : F⟮α + x✝ • x⟯ = F⟮α + y • x⟯
αxβ_in_K : α + x✝ • x ∈ F⟮α + x✝ • x⟯
αyβ_in_K : α + y • x ∈ F⟮α + x✝ • x⟯
β_in_K : x ∈ F⟮α + x✝ • x⟯
α_in_K : α ∈ F⟮α + x✝ • x⟯
⊢ x ∈ ↑F⟮α + x✝ • x⟯
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✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_finite : Fintype F
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
· exact exists_primitive_element_of_finite_bot F E

Goal state after:
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)
⊢ map (⊤.mulMap ↑I) (↑(LinearEquiv.rTensor (↥↑I) topEquiv.symm)).range = ⊤

Tactic:
LinearEquiv.range,

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)
⊢ map (⊤.mulMap ↑I) ⊤ = ⊤
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
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

pp: case mpr
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 ∈ (Units.map ↑(spanSingleton R)).range → I ∈ (unitsToPic R A).ker

Tactic:
<;>

Goal state after:
case mp
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

case mpr
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 ∈ (Units.map ↑(spanSingleton R)).range → I ∈ (unitsToPic R A).ker
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = ⋃ i, I

pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep (⋃ i, I)

Tactic:
<;>

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = ⋃ i, I

α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep (⋃ i, I)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
⊢ M ∈ (unitsToPic R A).range → M ∈ relPic R A

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
⊢ M ∈ relPic R A → M ∈ (unitsToPic R A).range

Tactic:
<;>

Goal state after:
case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
⊢ M ∈ (unitsToPic R A).range → M ∈ relPic R A

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
⊢ M ∈ relPic R A → M ∈ (unitsToPic R A).range
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ I = I ∪ I

pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep (I ∪ I)

Tactic:
<;>

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ I = I ∪ I

α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep (I ∪ I)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J ∪ I

pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep (J ∪ I)

Tactic:
<;>

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J ∪ I

α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep (J ∪ I)
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 (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})

Tactic:
exact hI.union_isBasis_union (h.subset subset_union_right).isBasis_self h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ Function.Injective fun x ↦ x * ↑(e 1)

Tactic:
convert! Subtype.val_injective.comp e.injective using 2

Goal state after:
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x✝ : R
⊢ x✝ * ↑(e 1) = (Subtype.val ∘ ⇑e) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case left
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ I = ⊤

pp: case right
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ J = ⊤

Tactic:
<;>

Goal state after:
case left
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ I = ⊤

case right
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit ↑(e 1)
⊢ J = ⊤
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.E = ∅ ↔ M = emptyOn α

Tactic:
simp only [emptyOn, ext_iff_indep, iff_self_and]

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E : Set α
⊢ (freeOn E)✶ = loopyOn E

Tactic:
by
  rw [freeOn, dual_dual]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.Finite
⊢ {N | N ≤r M} ⊆ (fun R ↦ M ↾ R) '' {b | b ⊆ M.E}

Tactic:
rintro _ ⟨R, hR, rfl⟩

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.Finite
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R ∈ (fun R ↦ M ↾ R) '' {b | b ⊆ M.E}
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ M, E = M.E ∧ M.Indep = Indep
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
obtain ⟨M, rfl, rfl⟩ := hex

Goal state after:
α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ M, E = M.E ∧ M.Indep = Indep
⊢ ∀ (I : Set α), Indep I → I ⊆ E

Tactic:
obtain ⟨M, rfl, rfl⟩ := hex

Goal state after:
α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ (I : Set α), M.Indep I → I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
hI' : M.IsBasis I (X ∩ Y)
hJ' : M.IsBasis J (X ∩ Y)
⊢ M.IsBasis I Y

Tactic:
exact hI'.transfer hJ' inter_subset_right hJ

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
← isRkFinite_inter_ground_iff

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
X : Set α
M : Matroid α
I : Set ↑X
⊢ (M.restrictSubtype X).Indep I ↔ M.Indep ↑I

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

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

Goal state before:
pp: α : Type u_1
X I : Set α
M : Matroid α
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M✶.comapOn (M.E ↓∩ M.E) Subtype.val = M✶.restrictSubtype M.E

pp: α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
← dual_ground,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M✶.comapOn (M✶.E ↓∩ M✶.E) Subtype.val = M✶.restrictSubtype M✶.E

α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
by
  by_cases he : e ∈ M.E
  · simp [isLoop_iff_closure_eq_loops_and_mem_ground, he]
  simp [← closure_inter_ground, singleton_inter_eq_empty.2 he, loops,
    (show ¬ M.IsNonloop e from fun h ↦ he h.mem_ground)]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.closure (X ∪ Y)) = M.eRk (X ∪ Y)

Tactic:
eRk_closure_eq

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∪ Y) = M.eRk (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
by
  obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
  obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
  obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
  rw [← hIX.eRk_eq_eRk_union, union_comm, ← hIY.eRk_eq_eRk_union, ← hIi.encard_eq_eRk,
    ← hIX.encard_eq_eRk, ← hIY.encard_eq_eRk, union_comm, ← encard_union_add_encard_inter, add_comm]
  exact add_le_add (eRk_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
⊢ M.eRk (M.closure Y) = M.eRk Y

Tactic:
eRk_closure_eq

Goal state after:
case pos
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
⊢ M.eRk Y = M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRank ≤ M.eRk X

Tactic:
← hB.encard_eq_eRk,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRank ≤ B.encard