mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
and_iff_right hI,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
rw [h]; exact M.empty_indep.isBasis_self

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

Tactic:
set B' := M.E \ X with hX

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
⊢ ∃ 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: α : Type u_1
M : Matroid α
B : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ M.E) B ↔ Maximal M.Indep B

Tactic:
maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ Maximal M.Indep B ∧ B ⊆ M.E ↔ Maximal M.Indep B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M.IsBasis (B ∩ (R ∩ M.E)) (R ∩ M.E)
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
hJ : M.IsBasis (B ∩ (R ∩ M.E)) (B ∩ (R ∩ M.E))
hIJ : I ⊆ B ∩ (R ∩ M.E)
he : I = B ∩ (R ∩ M.E)
⊢ M.IsBasis I (R ∩ M.E)

Tactic:
by rwa [he]

Goal state after:
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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
⊢ I.encard ≠ ⊤

Tactic:
rw [encard_ne_top_iff]

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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
⊢ I.Finite
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : (N ↾ range f).Indep (insert (f e) (f '' I))
he' : f e ∉ f '' I
heI : e ∉ I
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
rw [← image_insert_eq, restrict_indep_iff] at hei

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
he' : f e ∉ f '' I
heI : e ∉ I
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
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 : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
hi : M.Indep (insert f (B ∩ X))
⊢ False

Tactic:
exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

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.IsBase (M.E \ B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ M✶.IsBase B

Tactic:
dual_isBase_iff hB,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.IsBase (M.E \ B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ M.IsBase (M.E \ B)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

Tactic:
restrictSubtype,

Goal state after:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ ((M ↾ Y).comap Subtype.val).IsBasis I X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ (M.restrictSubtype X).IsBase B ↔ M.IsBasis' (Subtype.val '' B) X

Tactic:
restrictSubtype,

Goal state after:
α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ ((M ↾ X).comap Subtype.val).IsBase B ↔ M.IsBasis' (Subtype.val '' B) X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Tactic:
restrictSubtype,

Goal state after:
α : Type u_1
M : Matroid α
⊢ ((M ↾ M.E).comap Subtype.val)✶ = M✶.restrictSubtype M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M✶.comap 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:
restrictSubtype,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M✶.comap Subtype.val = (M✶ ↾ M✶.E).comap Subtype.val

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = M.eRk M.E

Tactic:
rw [eRk, restrict_ground_eq_self]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B

Tactic:
by
  refine ⟨fun h x hx heC ↦ (h.notMem_isCircuit <| hB.fundCircuit_isCircuit hx.1 hx.2) heC,
    fun h ↦ ?_⟩
  have h' : M.E \ {e} ⊆ M.closure (B \ {e}) := by
    rintro x ⟨hxE, hne : x ≠ e⟩
    obtain (hx | hx) := em (x ∈ B)
    · exact M.subset_closure (B \ {e}) (sdiff_subset.trans hB.subset_ground) ⟨hx, hne⟩
    have h_cct := (hB.fundCircuit_isCircuit hxE hx).mem_closure_sdiff_singleton_of_mem
      (M.mem_fundCircuit x B)
    refine (M.closure_subset_closure (subset_sdiff_singleton ?_ ?_)) h_cct
    · simpa using fundCircuit_subset_insert ..
    simp [hne.symm, h x ⟨hxE, hx⟩]
  rw [isColoop_iff_notMem_closure_compl (hB.subset_ground he)]
  exact notMem_subset (M.closure_subset_closure_of_subset_closure h') <|
    hB.indep.notMem_closure_sdiff_of_mem he

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
obtain ⟨I, hI⟩ := M✶.exists_isBasis X
  obtain ⟨B, hB, rfl⟩ := hI.exists_isBasis_inter_eq_of_superset hX
  have hB' : M✶.IsBase B := isBasis_ground_iff.1 hB
  have hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X) := by
    simpa using hB'.inter_isBasis_iff_compl_inter_isBasis_dual.1 hI
  rw [← hB'.compl_isBase_of_dual.encard_eq_eRank, hI.eRk_eq_encard, hd.eRk_eq_encard,
    ← encard_union_eq (by tauto_set), ← encard_union_eq (by tauto_set)]
  exact congr_arg _ (by tauto_set)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
X : Set α
⊢ M.closure (insert e (M.closure X)) = M.closure (insert e X)

Tactic:
simp_rw [← singleton_union, closure_union_closure_right_eq]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e X) = M.closure X

Tactic:
← closure_insert_closure_eq_closure_insert,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e (M.closure X)) = M.closure X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
⊢ C.Finite

Tactic:
have hi := hC.dep.not_indep
  rw [indep_iff_forall_finite_subset_indep] at hi; push Not at hi
  obtain ⟨J, hJC, hJfin, hJ⟩ := hi
  rwa [← hC.eq_of_not_indep_subset hJ hJC]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (M ↾ X).cRank ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
cRank

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (⨆ B, #↑↑B) ≤ lift.{u, v} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
and_iff_right hI,

Goal state after:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ M.E \ M.closure I ∨ e ∈ I ↔ e ∉ I → e ∈ M.E \ M.closure I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (M ↾ f '' X).cRank ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
cRank

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (⨆ B, #↑↑B) ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBase I

Tactic:
rw [← isBasis_ground_iff]; exact hI.isBasis_of_subset_of_subset_closure hI.subset_ground h

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBase I

Tactic:
by
  rw [← isBasis_ground_iff]; exact hI.isBasis_of_subset_of_subset_closure hI.subset_ground h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
hcard : #↑(f '' I \ (f '' J ∩ f '' I)) = #↑(f '' J \ (f '' J ∩ f '' I))
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)

Tactic:
sdiff_inter_self_eq_sdiff,

Goal state after:
α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
hcard : #↑(f '' I \ f '' J) = #↑(f '' J \ (f '' J ∩ f '' I))
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' I \ (f '' J ∩ f '' I) ∪ (f '' J ∩ f '' I) \ f '' (I ∩ J)) = #↑(f '' J \ f '' (J ∩ I))

Tactic:
sdiff_inter_self_eq_sdiff,

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' I \ f '' J ∪ (f '' J ∩ f '' I) \ f '' (I ∩ J)) = #↑(f '' J \ f '' (J ∩ I))
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (I ∩ J)) =
    #↑(f '' J \ (f '' I ∩ f '' J) ∪ (f '' I ∩ f '' J) \ f '' (J ∩ I))

pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
sdiff_inter_self_eq_sdiff,

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (I ∩ J)) = #↑(f '' J \ f '' I ∪ (f '' I ∩ f '' J) \ f '' (J ∩ I))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
⊢ ∃ B, M.IsBase B ∧ B.Finite

Tactic:
have ⟨B, hB⟩ := M.exists_isBase

Goal state after:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B.Finite
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank

Tactic:
← not_lt,

Goal state after:
α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ¬M.cRank < ℵ₀
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

Tactic:
by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

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

Goal state before:
pp: case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))

Tactic:
← closure_insert_closure_eq_closure_insert,

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (M.closure (I \ {e})))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case hC
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
x✝ : R
⊢ (((aeval x).comp (MvPolynomial.map (algebraMap R K))).comp C) x✝ = ((aeval x).comp C) x✝

Tactic:
simp [algebraMap_eq_smul_one]

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

Goal state before:
pp: case hX
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
i✝ : ι
⊢ ((aeval x).comp (MvPolynomial.map (algebraMap R K))) (X i✝) = (aeval x).toRingHom (X i✝)

Tactic:
simp [algebraMap_eq_smul_one]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (insert e (I \ {e}))

Tactic:
← closure_insert_closure_eq_closure_insert,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (insert e (M.closure (I \ {e})))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))

Tactic:
← closure_insert_closure_eq_closure_insert,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (M.closure (X ∩ M.E)))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (M.closure (X ∩ M.E)))
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)

Tactic:
simp_rw [trdeg, lift_iSup bddAbove_of_small]

Goal state after:
R : Type u_3
S : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ (⨆ i, lift.{v, u} #↑↑i) + ⨆ i, lift.{u, v} #↑↑i ≤ ⨆ i, lift.{u, v} #↑↑i
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)

Tactic:
← closure_insert_closure_eq_closure_insert,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (M.closure (insert f (M.closure (insert e X)))) = M.closure (insert e X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ X ∩ E ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I

Tactic:
inter_assoc (c := E),

Goal state after:
α : Type u_2
I E X : Set α
⊢ X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

pp: case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ (∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e

Tactic:
· rintro ⟨⟨x, hxE, rfl⟩, h2⟩
    refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩
    obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm
    rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy
    rwa [← hfy]

Goal state after:
case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ (∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : fixedBy α g = Set.univ
comm : Commute g h
⊢ g = 1

Tactic:
fixedBy_eq_univ_iff_eq_one

Goal state after:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : g = 1
comm : Commute g h
⊢ g = 1
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R (⇑(algebraMap S A) ∘ x)

Tactic:
by
  let f := IsScalarTower.toAlgHom R S A
  refine hx.1.map (f := f) (FaithfulSMul.algebraMap_injective S A).injOn
    |>.isTranscendenceBasis_iff_isAlgebraic.mpr ?_
  rw [Set.range_comp, ← AlgHom.map_adjoin]
  set Rx := adjoin R (range x)
  let e := Rx.equivMapOfInjective f (FaithfulSMul.algebraMap_injective S A)
  let := e.toRingHom.toAlgebra
  have : IsScalarTower Rx (Rx.map f) A := .of_algebraMap_eq fun x ↦ rfl
  have : Algebra.IsAlgebraic Rx S := hx.isAlgebraic
  have : Algebra.IsAlgebraic Rx A := .trans _ S _
  exact .extendScalars e.injective

Goal state after: