mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = f ⟨x, hx⟩

Tactic:
dif_pos hx

Goal state after:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₁
⊢ f ⟨x, hx⟩ = f ⟨x, hx⟩
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨x, hx⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, hx⟩ = f₁ ⟨↑x, hx⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, hx⟩ = f₂ ⟨↑x, hx⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := ⋯.some
⊢ finrank R (M × N) = n + 1

Tactic:
have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := ⋯.some
h1 : rankAtStalk M 𝔭 = 1
⊢ finrank R (M × N) = n + 1
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := ⋯.some
h1 : rankAtStalk M 𝔭 = 1
heq : ↑(finrank R (M × N)) = 1 + ↑(finrank R N)
⊢ finrank R (M × N) = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝² : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝¹ : IsScalarTower R (Localization S) Rₚ
this✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
r : R
r' : Localization S
m : Mₚ
⊢ r •
      (algebraMap (Localization S) (Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))) r' •
        m =
    r • r' • m

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁵ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁴ : IsScalarTower R (Localization S) Rₚ
this✝³ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝² : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝¹ : IsScalarTower R (Localization S) Mₚ
this✝ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this : IsLocalizedModule p.asIdeal.primeCompl l
⊢ Free Rₚ Mₚ ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Tactic:
induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝² : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝¹ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝ : IsScalarTower R (Localization.Away f) Rₚ
this : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
r : R
r' : Localization.Away f
m : Mₚ
⊢ r • (algebraMap (Localization.Away f) (Localization.AtPrime p.asIdeal)) r' • m = r • r' • m

Tactic:
rfl

Goal state after:
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
e : M ⊗[R] N ≃ₗ[R] R
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (contractLeft R N ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ↑e) x✝¹) x✝

Tactic:
rfl

Goal state after:
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
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let aux := finsuppRight R _ M N S ≪≫ₗ Finsupp.mapRange.linearEquiv e

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
⊢ Module.Finite R M ∧ Projective R M
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Surjective ⇑(LinearMap.lTensor M f)
⊢ Function.Surjective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)

Tactic:
simpa using LinearMap.lTensor_surjective _ h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)

Tactic:
mk_tensor,

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = Pic.mk R M.AsModule * Pic.mk R N.AsModule
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:
mk_tensor,

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 * Pic.mk R x✝.AsModule = x✝¹ * x✝
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:
rfl

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

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

Tactic:
by
  simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_ofPred]

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

Goal state before:
pp: α : 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'
hIB' : f ∈ B' ∧ B \ {e} ⊆ B'
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
← sdiff_eq_empty,

Goal state after:
α : 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'
hIB' : f ∈ B' ∧ (B \ {e}) \ B' = ∅
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))
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:
rfl

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

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

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

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

Tactic:
refine h_ind.isBasis_of_forall_insert
    (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_
  rintro e ⟨⟨_, ⟨⟨i, hi, rfl⟩, (hes : e ∈ X i)⟩⟩, he'⟩
  rw [mem_iUnion, not_exists] at he'
  refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_
  rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]
  exact (hI i).subset_ground hes

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x✝¹ : ↥⊤
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry (⊤.mulMap (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ↑(LinearEquiv.rTensor (↥(submoduleAlgebra e)) Submodule.topEquiv ≪≫ₗ
              LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)))
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
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
x✝¹ : ↥I
x✝ : ↥(submoduleAlgebra e)
⊢ ((AlgebraTensorModule.curry ((I * submoduleAlgebra e).subtype ∘ₗ I.mulMap' (submoduleAlgebra e))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (tensorSubmoduleAlgebraEquiv e)) ∘ₗ
            LinearMap.rTensor (↥(submoduleAlgebra e)) I.subtype))
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
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:
mk_tensor,

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 * Pic.mk R M⁻¹.AsModule = 1
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶.E = ∅

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Tactic:
rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, and_iff_left_iff_imp]
  exact fun h ↦ h.trans hIE

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

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
⊢ B = E \ I

Tactic:
rw [← sdiff_sdiff_cancel_left hB, h, sdiff_inter_self_eq_sdiff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E → ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
grind

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (True → True) ∧ I ⊆ f ⁻¹' N.E

Tactic:
implies_true,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ True ∧ I ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Dual

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

Tactic:
and_comm (a := (_ : Set α) ⊆ _),

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ Disjoint X B) ∧ X ⊆ M.E ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ B, M.IsBase B ∧ Disjoint X B) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)

Tactic:
exact fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩,
    fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
← hJ'.encard_eq_encard hb

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False
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
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
by
  obtain ⟨I, hI, hIfin⟩ := hX.exists_finite_isBasis'
  obtain ⟨J, hJ, hJfin⟩ := hY.exists_finite_isBasis'
  rw [← isRkFinite_inter_ground_iff]
  refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_
  rw [closure_union_congr_left hI.closure_eq_closure,
    closure_union_congr_right hJ.closure_eq_closure]
  exact inter_ground_subset_closure M (X ∪ Y)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = (fun a ↦ f ↑a) '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
← image_image f Subtype.val,

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = f '' Subtype.val '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
obtain ⟨I₀, hI₀, rfl⟩ := hI
  exact ⟨I₀, hI₀, (hf.mono hI₀.subset_ground).bijOn_image⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.map f hf).IsBase (f '' B) ↔ M.IsBase B

Tactic:
by
  rw [map_isBase_iff]
  refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩
  rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ; rwa [hIJ]

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Tactic:
by
  simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_sdiff, and_iff_right he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α ↪ β
⊢ (M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e

Tactic:
by
  simp [mapEmbedding, isLoop_iff, isLoop_iff, map_closure_eq, preimage_empty, ← closure_empty]

Goal state after: