mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
⊢ i = j

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = j

case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = j
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ ∀ (r : R) (f : (i : ι) → s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (r • (tprod R) f)) = r • (tprod R) f

Tactic:
intro x y
      simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]
      congr
      aesop

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
i : Fin (Nat.succ 0).succ
⊢ ↑(![↑a, ↑b] i) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) i)

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ Free R P

Tactic:
by
  have := Module.finitePresentation_of_free_of_surjective g hg
    (by rw [h.linearMap_ker_eq, LinearMap.range_eq_map]; exact (Module.Finite.fg_top).map f)
  apply free_of_maximalIdeal_rTensor_injective
  rw [← LinearMap.lTensor_inj_iff_rTensor_inj]
  apply lTensor_injective_of_exact_of_exact_of_rTensor_injective
    h hg (LinearMap.exact_subtype_mkQ 𝔪) (Submodule.mkQ_surjective _)
    ((LinearMap.lTensor_inj_iff_rTensor_inj _ _).mp hf)
    (Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : (∃ l_1, l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ l.range.subtype = LinearMap.id
⊢ Projective R ↥l.range

Tactic:
obtain ⟨l', hl'⟩ := this.mp
         (Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _))

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : (∃ l_1, l.range.mkQ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ l.range.subtype = LinearMap.id
l' : N →ₗ[R] ↥l.range
hl' : l' ∘ₗ l.range.subtype = LinearMap.id
⊢ Projective R ↥l.range
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∃ a ∈ p.primeCompl, ∃ y k, f y = a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''

Tactic:
obtain ⟨a, ha, y, k, h⟩ := h

Goal state after:
case pos
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ x, P = ⊥.colon {x}
hx : ⊥.colon {x} ≤ P
⊢ r ∈ ⋃ p, ⋃ (_ : p.IsPrime ∧ ∃ x, p = ⊥.colon {x}), ↑p

Tactic:
exact Set.mem_iUnion₂_of_mem hP (hx (by rwa [mem_colon_singleton]))

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : Kˣ
⊢ spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1

Tactic:
simp only [spanSingleton_one, Units.inv_mul', spanSingleton_mul_spanSingleton]

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ { toFun := fun x ↦ { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
          map_one' := ⋯, map_mul' := ⋯ }
        x =
      I ↔
    spanSingleton R⁰ ↑x = ↑I

Tactic:
exact Units.ext_iff

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (U.mulIndicator ⇑f ⁻¹' s)

Tactic:
rw [mulIndicator_preimage, Set.ite, Set.sdiff_eq]
    exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ (derivedSeries G n).Characteristic

Tactic:
induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ normalClosure F K ↥(normalClosure F K L) = ⊤

Tactic:
normalClosure,

Goal state after:
case right
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
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ⨆ f, f.fieldRange = ⊤
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case inl
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
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥(normalClosure F K L)

Tactic:
normalClosure,

Goal state after:
case inl
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
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥(⨆ f, f.fieldRange)
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:
DFunLike.ext'_iff

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.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ (M.E \ B)ᶜ
⊢ I ⊆ B

pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
sdiff_eq,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ (M.E ∩ Bᶜ)ᶜ
⊢ I ⊆ B

case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inl
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_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
have base : P ⊥ := ⟨0, adjoin_zero⟩

Goal state after:
case inl
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_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
⊢ ∃ α, F⟮α⟯ = ⊤
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B' I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
obtain ⟨I₀, hI₀I, hI₀fin, hI₀card⟩ := h.exists_subset_ncard_eq (B.ncard + 1)

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
⊢ False
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:
adjoin_simple_adjoin_simple,

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⟯ = F⟮α, β⟯
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : 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 α := M.E \ X
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) \ I)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
sdiff_eq,

Goal state after:
α : 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 α := M.E \ X
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) ∩ Iᶜ)ᶜ ⊆ B''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ I
⊢ M.IsBasis I (insert e I)

Tactic:
rw [insert_eq_of_mem he]; exact hI.isBasis_self

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
e : α
heX : e ∈ X
heI' : e ∈ I'
heI : e ∉ I
⊢ False

Tactic:
exact heI <| hI.mem_of_insert_indep heX (hI'.indep.subset (insert_subset heI' hII'))

Goal state after:
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:
simp_rw [← mul_assoc, top_mul_submoduleAlgebra] at 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 :
  ⊤ =
    ⊤ *
      (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: case refine_1
α : 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
⊢ Disjoint I' B'

Tactic:
exact Disjoint.mono_right hB'IB <| disjoint_union_right.2
        ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩

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

Goal state before:
pp: case h
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ ∀ ⦃t : Set α⦄, M.Indep t → t ⊆ R → t ⊆ A → J ⊆ t → J = t

Tactic:
exact fun K hK _ hKA hJK ↦ hJ.eq_of_subset_indep hK hJK hKA

Goal state after:
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 : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ (X \ J) ⊆ B'

Tactic:
sdiff_eq,

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 : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ (X ∩ Jᶜ) ⊆ B'
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 : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ (B'' ∩ X) \ B' ⊆ J

Tactic:
sdiff_eq,

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 : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ∩ B'ᶜ ⊆ J
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : M.E \ (B ∪ X) ∩ B' = ∅ ∧ e ∉ B'
⊢ False

Tactic:
sdiff_eq,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : M.E ∩ (B ∪ X)ᶜ ∩ B' = ∅ ∧ e ∉ B'
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
⊢ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀

pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B

Tactic:
· obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map
    refine ⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩
    rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]
    exact h.eq_of_subset (hJ.map f hf) (hbij.image_eq ▸ image_mono hB₀J)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
simp only [Dep, map_indep_iff, not_exists, not_and, map_ground, subset_image_iff]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔ ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
by
  rw [restrict_eRk_eq', inter_eq_self_of_subset_left h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)
    rw [isCircuit_iff_dep_forall_sdiff_singleton_indep, dep_iff, insert_subset_iff,
      and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]
    suffices ¬ M.Indep {e, f} by simpa [pair_sdiff_left hef, hf, pair_sdiff_right hef, he]
    rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]
    simp [← h, mem_closure_self _ _ he.mem_ground]
  have hclosure := (h.closure_sdiff_singleton_eq e).trans
    (h.closure_sdiff_singleton_eq f).symm
  rwa [pair_sdiff_left hef, pair_sdiff_right hef, eq_comm] at hclosure

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

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
j : ι
he : x j ∈ C j \ {x j}
⊢ False

Tactic:
simp at he

Goal state after: