mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
⊢ motive M

Tactic:
by
  have equiv (N₁ : Type v) [AddCommGroup N₁] [Module A N₁] [Module.Finite A N₁]
      (N₂ : Type v) [AddCommGroup N₂] [Module A N₂] [Module.Finite A N₂]
      (f : N₁ ≃ₗ[A] N₂) (h : motive N₁) : motive N₂ :=
    exact N₁ N₂ PUnit.{v + 1} f 0 f.injective (Function.surjective_to_subsingleton _)
      ((f.exact_zero_iff_surjective _).2 f.surjective) h (subsingleton _)
  obtain ⟨s, hs1, hs2⟩ := IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime A M
  suffices H : ∀ n, (h : n < s.length + 1) → motive (s ⟨n, h⟩) by
    replace H : motive s.last := H s.length s.length.lt_add_one
    rw [hs2] at H
    exact equiv _ _ Submodule.topEquiv H
  intro n h
  induction n with
  | zero =>
    change motive s.head
    rw [hs1]
    exact subsingleton _
  | succ n ih =>
    specialize ih (n.lt_add_one.trans h)
    obtain ⟨hle, p, ⟨f⟩⟩ := s.step ⟨n, (add_lt_add_iff_right _).1 h⟩
    replace ih := equiv _ _ (Submodule.submoduleOfEquivOfLe hle).symm ih
    exact exact _ _ _ _ _ (Submodule.injective_subtype _) (Submodule.mkQ_surjective _)
      (LinearMap.exact_subtype_mkQ _) ih (quotient _ p f)

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
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : FractionalIdeal R⁰ K
hI : IsUnit I
⊢ (↑I).IsPrincipal

Tactic:
rcases hI with ⟨I, rfl⟩
  rw [← ClassGroup.mk_eq_one_iff, Subsingleton.elim (ClassGroup.mk K I) 1]

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✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ IsOpen[inst✝] ((fun x a ↦ (f a) x) ⁻¹' {g})

Tactic:
have : (fun (x : X) (a : α) => f a x) ⁻¹' {g} = ⋂ a : α, f a ⁻¹' {g a} := by
      ext; simp [funext_iff]

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
this : (fun x a ↦ (f a) x) ⁻¹' {g} = ⋂ a, ⇑(f a) ⁻¹' {g a}
⊢ IsOpen[inst✝] ((fun x a ↦ (f a) x) ⁻¹' {g})
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₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Tactic:
rw [piecewise', piecewise_apply_right (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]

Goal state after:
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⟩
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
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let g' : M →ₗ[R] S →₀ R := aux ∘ₗ g.lTensor M ∘ₗ (TensorProduct.rid R M).symm

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
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
g' : M →ₗ[R] ↥S →₀ R := ↑aux ∘ₗ LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.rid R M).symm
⊢ Module.Finite R M ∧ Projective R M
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
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
g' : M →ₗ[R] ↥S →₀ R := ↑aux ∘ₗ LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.rid R M).symm
this : Function.Surjective ⇑f'
⊢ Module.Finite R M ∧ Projective R M

Tactic:
refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩

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
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
g' : M →ₗ[R] ↥S →₀ R := ↑aux ∘ₗ LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.rid R M).symm
this : Function.Surjective ⇑f'
m : M
⊢ (f' ∘ₗ g') m = LinearMap.id m
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
hx : ∀ (i : ι), ∀ x_1 ∈ (minpoly F x).rootSet K, x_1 ∈ t i
⊢ ∀ x_1 ∈ (minpoly F x).rootSet K, x_1 ∈ ⨅ i, t i

Tactic:
rintro y hy - ⟨-, ⟨i, rfl⟩, rfl⟩

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
hx : ∀ (i : ι), ∀ x_1 ∈ (minpoly F x).rootSet K, x_1 ∈ t i
y : K
hy : y ∈ (minpoly F x).rootSet K
i : ι
⊢ y ∈ (fun x ↦ ↑x) ((fun i ↦ t i) i)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ M.RankPos

Tactic:
rw [rankPos_iff]
  intro he
  obtain rfl := he.eq_of_subset_isBase hB (empty_subset B)
  simp at h

Goal state after:
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})
hf : Function.Injective f
⊢ f '' {M | M.E ⊆ E} ⊆ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}

Tactic:
rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩

Goal state after:
α : Type u_1
E : Set α
hE✝ : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M ↦ (M.E, {B | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ f M ∈ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X

Tactic:
rw [isBasis_iff]

Goal state after:
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
by
  rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]

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 ∧ I ⊆ f ⁻¹' N.E

Tactic:
true_and

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
    refine ⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩
    simp only [mem_sdiff, mem_image, not_exists, not_and] at he
    obtain ⟨⟨e, heX, rfl⟩, he⟩ := he
    have heI : e ∉ I := fun heI ↦ (he e heI rfl)
    replace h := h.insert_dep ⟨heX, heI⟩
    simp only [comap_dep_iff, image_insert_eq, or_iff_not_imp_right, injOn_insert heI,
      hinj, mem_image, not_exists, not_and, true_and, not_forall, not_not] at h
    exact h (fun _ ↦ he)
  refine Indep.isBasis_of_forall_insert ?_ h.2.2 fun e ⟨heX, heI⟩ ↦ ?_
  · simp [comap_indep_iff, h.1.indep, h.2]
  have hIE : insert e I ⊆ (N.comap f).E := by
      simp_rw [comap_ground_eq, ← image_subset_iff]
      exact (image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground
  suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
    by simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]
  exact h.1.mem_of_insert_indep (mem_image_of_mem f heX)

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✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
hfin : (f '' J).Finite
J' : Set α
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
⊢ N.Indep (f '' J)

Tactic:
← hJ'.image_eq

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
J : Set α
hJ : J ⊆ I
J' : Set α
hfin : (f '' J').Finite
hJ'J : J' ⊆ J
hJ' : BijOn f J' (f '' J)
⊢ N.Indep (f '' J')
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
exact ⟨y, hy, by rwa [isBase_restrict_iff] at h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶ = N✶.comapOn E f

Tactic:
refine ext_isBase (by simp) (fun B hB ↦ ?_)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.IsBase B ↔ (N✶.comapOn E f).IsBase B
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl
  tfae_have 2 ↔ 3 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e),
    isCircuit_def, minimal_iff_forall_ssubset, ssubset_singleton_iff]
  tfae_have 2 ↔ 4 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]
  tfae_have 4 ↔ 5 := by
    simp only [dep_iff, singleton_subset_iff, mem_sdiff, forall_and]
    refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
    obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset
    exact h.2 _ hB (by simpa using heB)
  tfae_finish

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.E \ M.loops = {e | M.IsNonloop e}

Tactic:
simp [Set.ext_iff, isNonloop_iff, and_comm, isLoop_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk X + M.eRk {e} ≤ M.eRk X + 1

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Mathlib.Tactic.GCongr.gcongr "gcongr" [] [])
    ";"
    (Tactic.simpa
     "simpa"
     []
     []
     (Tactic.simpaArgsRest
      (Tactic.optConfig [])
      []
      []
      []
      ["using"
       (Term.app
        `M.eRk_le_encard
        [(choice
          («term{_}» "{" [`e] "}")
          (Term.structInst
           "{"
           []
           (Term.structInstFields [(Term.structInstField (Term.structInstLVal `e []) [])])
           (Term.optEllipsis [])
           []
           "}"))])]))])))

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

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

Tactic:
rw [closure, sInter_eq_iInter]

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ i, ↑i)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (loopyOn X).eRank = 0

Tactic:
rw [eRank_def, eRk_loopyOn]

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

Goal state before:
pp: α : Type u_1
X Y : Set α
hXY : X ⊆ Y
⊢ (freeOn Y).eRk X = X.encard

Tactic:
by
  obtain ⟨I, hI⟩ := (freeOn Y).exists_isBasis X
  rw [hI.eRk_eq_encard, (freeOn_indep hXY).eq_of_isBasis hI]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.closure (M.E \ K)

Tactic:
← hKe.closure_eq,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ (K \ {e})) ⊆ M.closure (M.E \ K)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ {e | (M ↾ univ).IsNonloop e} = M.removeLoops

Tactic:
removeLoops_eq_restrict

Goal state after:
α : Type u_1
M : Matroid α
⊢ M ↾ {e | (M ↾ univ).IsNonloop e} = M ↾ {e | M.IsNonloop e}
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Infinite
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
← infinite_coe_iff

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
⊢ #↑(B \ B') ≤ #↑(B' \ B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) ⊆ M.closure I

Tactic:
apply closure_subset_closure_of_subset_closure

Goal state after:
case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ insert f I \ {e} ⊆ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure I ⊆ M.closure (insert f I \ {e})

Tactic:
apply closure_subset_closure_of_subset_closure

Goal state after:
case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ I ⊆ M.closure (insert f I \ {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
⊢ ⨆ i, ⨆ j, lift.{v, u} #↑↑i + lift.{u, v} #↑↑j ≤ ⨆ i, lift.{u, v} #↑↑i

Tactic:
add_comm (lift.{v, u} _),

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, ⨆ j, lift.{u, v} #↑↑j + lift.{v, u} #↑↑i ≤ ⨆ i, lift.{u, v} #↑↑i
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
convert! e.symm.isTranscendenceBasis hx

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ x = ⇑e.symm ∘ ⇑e ∘ x
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
this : Algebra.IsAlgebraic ↥Rt ↥St
⊢ Transcendental (↥St) (x i)

Tactic:
exact (hx.transcendental_adjoin hi).extendScalars _

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

Goal state before:
pp: 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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this✝² : Algebra.IsAlgebraic S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this✝¹ : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this✝ : IsScalarTower (↥Rv) (↥Sv) A
this : Nontrivial R
⊢ Algebra.IsAlgebraic S A

Tactic:
have := hv.isAlgebraic

Goal state after:
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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this✝³ : Algebra.IsAlgebraic S ↥Sv
le : Rv ≤ Subalgebra.restrictScalars R Sv
this✝² : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this✝¹ : IsScalarTower (↥Rv) (↥Sv) A
this✝ : Nontrivial R
this : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
⊢ Algebra.IsAlgebraic S A
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
x : AlgebraicClosure F
hx : (aeval x) u = 0
⊢ (aeval x) f = 0

Tactic:
simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L,
    z ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup

Tactic:
have : FiniteDimensional K E1 := h_E1

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
this : FiniteDimensional K ↥E1
⊢ ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L,
    z ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup Gal(L/K)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g ↦ g.carrier) H * (fun g ↦ g.carrier) H ⊆ (fun g ↦ g.carrier) H

Tactic:
rintro x ⟨a, haH, b, hbH, rfl⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup Gal(L/K)
left✝ : H ∈ fixedByFinite K L
a : Gal(L/K)
haH : a ∈ (fun g ↦ g.carrier) H
b : Gal(L/K)
hbH : b ∈ (fun g ↦ g.carrier) H
⊢ (fun x1 x2 ↦ x1 * x2) a b ∈ (fun g ↦ g.carrier) H