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

Goal state before:
pp: case e'_2
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' : 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0
hb' : 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0
⊢ 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ + 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩

Tactic:
← tmul_add

Goal state after:
case e'_2
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝¹⁶ : CommRing R''
inst✝¹⁵ : CommRing S''
inst✝¹⁴ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' : 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0
hb' : 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0
⊢ 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 1 ⊗ₜ[P.Ring] (⟨a, ⋯⟩ + ⟨b, ⋯⟩)
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace

Tactic:
by
  letI := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
  haveI : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' rfl
  letI := f.toAlgHom.toAlgebra
  haveI : IsScalarTower P.Ring P'.Ring S' :=
    IsScalarTower.of_algebraMap_eq (fun x ↦ (f.algebraMap_toRingHom x).symm)
  apply LinearMap.liftBaseChange
  refine (TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0

Tactic:
and_comm

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ (∀ m ∈ s, ∃ x ∉ p.asIdeal, x • m = 0) → ∀ x ∈ s, ∃ r ∈ p.asIdeal.primeCompl, r • x = 0
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
x : N
hs' : ∃ a_1, ∃ z ∈ Submodule.span R' ↑s, x = a_1 • a + z
⊢ ∃ t a_1, ∃ z ∈ Submodule.span R ↑s, t • x = a_1 • a + z

Tactic:
rcases hs' with ⟨y, z, hz, rfl⟩

Goal state after:
case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
v : Fin n → M
this : (Matrix.of fun i j ↦ (f j) (v i)).det = 0
⊢ (LinearMap.compAlternatingMap
        (((toTensorPower R M n).dualMap.compMultilinearMap (TensorPower.multilinearMapToDual R M n)).toFun f)
        (ιMulti R n))
      v =
    (LinearMap.compAlternatingMap 0 (ιMulti R n)) v

Tactic:
by
      simpa [Matrix.det_apply] using this

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : 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
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
z₁ z₂ : R
f : (i : ι) → s i
⊢ (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z₁, f) + FreeAddMonoid.of (z₂, f)) =
    (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z₁ + z₂, f))

Tactic:
by simp [FreeAddMonoid.lift_eval_of, C_add_scalar]

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

Goal state before:
pp: case insert.specialize_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ (Ideal.Quotient.mk 𝔪) ((-if True then 0 else a' ↑n) * ↑hj.unit⁻¹) = 0

Tactic:
if_pos,

Goal state after:
case insert.specialize_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ (Ideal.Quotient.mk 𝔪) (-0 * ↑hj.unit⁻¹) = 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ (x y : ⨂[R] (i : ι), s i),
    (liftAux φ) (r • x) = r • (liftAux φ) x →
      (liftAux φ) (r • y) = r • (liftAux φ) y → (liftAux φ) (r • (x + y)) = r • (liftAux φ) (x + y)

Tactic:
intro z y ihz ihy

Goal state after:
case refine_2
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : (liftAux φ) (r • z) = r • (liftAux φ) z
ihy : (liftAux φ) (r • y) = r • (liftAux φ) y
⊢ (liftAux φ) (r • (z + y)) = r • (liftAux φ) (z + y)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
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ˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
exact ⟨x, hx⟩

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

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y

Tactic:
· exact ⟨Classical.arbitrary Y, funext <| h.elim⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y
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
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ freeLocus R M = freeLocus R M'

Tactic:
ext p
  exact mem_freeLocus_of_isLocalization _ _ _
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M' ∘ₗ e.toLinearMap)

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✝² : Module.Invertible R M✝
inst✝¹ : Module.Invertible R N
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (Invertible.linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ 1 = ∑ i ∈ S, i.1 i.2

Tactic:
simpa [LinearEquiv.symm_apply_eq, Invertible.linearEquiv] using hS

Goal state after:
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₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [normalClosure_le_iff] at h
    simpa only [fieldRange_val] using h K₁.val
  · rw [← normalClosure_of_normal K₂]
    exact normalClosure_mono K₁ K₂ h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.encard = B₂.encard

Tactic:
by
  rw [M.isBase_exchange.encard_isBase_eq hB₁ hB₂]

Goal state after:
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 • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1

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⟮α + x • β⟯
β_in_K : (x - y) • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (¬M.Indep I → ¬I ⊆ M.E) ∧ I ⊆ M.E

Tactic:
not_imp_not

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

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

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ False
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 α
⊢ M.Indep x✝ ↔ ∃ B, M.IsBase B ∧ x✝ ⊆ B

Tactic:
M.indep_iff

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M.IsBasis I I ↔ M.Indep I

Tactic:
rw [isBasis_iff', and_iff_right rfl.subset, and_assoc, and_iff_left_iff_imp]
  exact fun hi ↦ ⟨fun _ _ ↦ subset_antisymm, hi.subset_ground⟩

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

Goal state before:
pp: α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis I ∅

Tactic:
rw [h]

Goal state after:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : (∀ (x : Set α), x ∈ {B | M.IsBase B} ↔ x ∈ {B | M'.IsBase B}) ∧ M.E = M'.E
⊢ M = M'

Tactic:
and_comm

Goal state after:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : M.E = M'.E ∧ ∀ (x : Set α), x ∈ {B | M.IsBase B} ↔ x ∈ {B | M'.IsBase B}
⊢ M = M'
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
⊢ (insert e I₀).ncard ≤ J.ncard

Tactic:
refine not_lt.1 fun hlt ↦ ?_

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hlt : J.ncard < (insert e I₀).ncard
⊢ False
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I

Tactic:
by
  rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]

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

Goal state before:
pp: case refine_4
α : 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
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ Disjoint J B'

Tactic:
obtain rfl : B₁ = B' := by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

Goal state after:
case refine_4
α : 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
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
⊢ Disjoint J B₁
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E).E \ B = I ∩ E ↔ B = E \ I

Tactic:
uniqueBaseOn_ground

Goal state after:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ E \ B = I ∩ E ↔ B = E \ I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X)
hIX : I ⊆ X
hX : X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀

Tactic:
obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' ⇑f '' X) ∧ I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' ⇑f '' X)
hIX : I ⊆ ⇑f '' X
hX : ⇑f '' X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
    simpa [fundCircuit_eq_sInter hecl, hne, ← insert_sdiff_singleton_comm hne.symm,
      (hI.sdiff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]

Goal state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ ¬M.IsLoop f ∧ f ∈ M.E

Tactic:
and_comm

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ f ∈ M.E ∧ ¬M.IsLoop f
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl
  tfae_have 1 ↔ 3 := singleton_isCocircuit.symm
  tfae_have 1 ↔ 4 := by
    simp_rw [← dual_isLoop_iff_isColoop, isLoop_iff_forall_mem_compl_isBase]
    refine ⟨fun h B hB ↦ ?_, fun h B hB ↦ h hB.compl_isBase_of_dual⟩
    obtain ⟨-, heB : e ∈ B⟩ := by simpa using h (M.E \ B) hB.compl_isBase_dual
    assumption
  tfae_have 3 → 5 := fun h ↦
    ⟨fun C hC heC ↦ hC.inter_isCocircuit_ne_singleton h (e := e) (by simpa), h.subset_ground rfl⟩
  tfae_have 5 → 4 := by
    refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
    rw [← hB.closure_eq] at heE
    obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE
    exact h hC heC
  tfae_have 5 ↔ 6 := by
    refine ⟨fun h X ↦ ⟨fun heX ↦ by_contra fun heX' ↦ ?_, fun heX ↦ M.mem_closure_of_mem' heX h.2⟩,
      fun h ↦ ⟨fun C hC heC ↦ ?_, M.closure_subset_ground _ <| (h {e}).2 rfl⟩⟩
    · obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX
      exact h.1 hC heC
    · simpa [hC.mem_closure_sdiff_singleton_of_mem heC] using h (C \ {e})
  tfae_have 1 ↔ 7 := by
    wlog he : e ∈ M.E
    · exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]
    rw [spanning_iff_compl_coindep sdiff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      sdiff_sdiff_cancel_left (by simpa), ← not_indep_iff (by simpa)]
  tfae_finish

Goal state after: