mathlib-initiative/mathlib-tactics huggingface dataset:
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
    left
    refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
    · rw [hx] at hb
      obtain ⟨n, hb⟩ := hb
      use n
      rw [mem_colon_singleton, mem_bot] at hb ⊢
      apply_fun _ using hf
      rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
    · rw [mem_colon_singleton, mem_bot] at hb
      apply_fun f at hb
      rw [map_smul, map_zero, h, ← mul_smul, ← mem_bot R, ← mem_colon_singleton] at hb
      replace hb := hx.ge (Ideal.le_radical hb)
      contrapose hb
      exact p.primeCompl.mul_mem (p.primeCompl.pow_mem hb n) (p.primeCompl.pow_mem ha k)

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

Goal state before:
pp: case inr
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✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ n.gcd (Fintype.card (ClassGroup R))

Tactic:
Nat.dvd_gcd_iff

Goal state after:
case inr
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✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) ∣ n ∧ orderOf ((ClassGroup.mk K) u) ∣ Fintype.card (ClassGroup R)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n.gcd (Fintype.card (ClassGroup R))

Tactic:
Nat.dvd_gcd_iff

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n ∧ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ Fintype.card (ClassGroup R)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
i : Bool
⊢ IsClosed[inst✝¹] (bif i then C₁ else C₂)

Tactic:
cases i <;> [exact h₂; exact h₁]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Polynomial.aeval ((Algebra.lmul A B) x)) f = 0
⊢ (Polynomial.aeval x) f = 0

Tactic:
rw [aeval_algHom_apply] at f_aeval

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Module.Finite A B
x : B
f : A[X]
f_monic : f.Monic
f_deg : f.natDegree = ⊤.spanFinrank
f_aeval : (Algebra.lmul A B) ((Polynomial.aeval x) f) = 0
⊢ (Polynomial.aeval x) f = 0
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G ≠ ⊤

Tactic:
obtain ⟨n, hn⟩ := hG

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ _root_.commutator G ≠ ⊤
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_2
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₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂

Tactic:
← normalClosure_of_normal K₂

Goal state after:
case refine_2
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₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ normalClosure F (↥K₂) L
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
y : K
hy : y ∈ (minpoly F x).rootSet K
i : ι
⊢ y ∈ (fun x ↦ ↑x) ((fun i ↦ t i) i)

Tactic:
exact hx i y hy

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
⊢ ∀ (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)

Tactic:
β

Goal state after:
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 ⊥
K : IntermediateField F E
β : E
⊢ P K → P (IntermediateField.restrictScalars F (↥K)⟮β⟯)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : (aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α

pp: case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : ¬(aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α

Tactic:
· simp only [hzero, div_zero, pow_eq_zero_iff hm] at h
    exact h.symm ▸ isAlgebraic_zero

Goal state after:
case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : ¬(aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
⊢ ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)

Goal state after:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
B' : Set α
hB' : M.IsBasis B' (I ∪ B)
hIB' : I ⊆ B'
⊢ ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) j → Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K ↦ P K ∧ K ⊆ X) K
hYK : Y ⊆ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K.ncard ≤ Y.ncard

Tactic:
exact hY' ⟨hPK, hIY.trans hYK, hKX⟩ (ncard_le_ncard hYK hKfin)

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:
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 : α → β
⊢ ∀ X ⊆ f ⁻¹' N.E, ExistsMaximalSubsetProperty (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) X

Tactic:
rintro X - I ⟨hI, hIinj⟩ hIX

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N <r M
⊢ N ≠ M

Tactic:
rintro rfl; rw [← ofMatroid_lt_iff] at h; simp at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.IsBase I
hNM : N ≤r M
⊢ M.IsBasis I N.E

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM; rwa [isBase_restrict_iff] at hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

Tactic:
isRkFinite_singleton.isRkFinite_sdiff_iff

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite X ↔ M.IsRkFinite X
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
by
  obtain rfl | hne := eq_or_ne x e
  · simp [hI.sdiff, mem_fundCircuit]
  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]
  refine ⟨fun h hecl ↦ (h _ sdiff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
  exact M.closure_subset_closure (subset_sdiff_singleton hJ hxJ) heJ

Goal state after:
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:
rw [restrictSubtype, comap_isBase_iff]
  simp [Subtype.val_injective.injOn, isBasis_restrict_iff',
    isBasis'_iff_isBasis_inter_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
  rw [← eRk_inter_ground, ← hI.encard_eq_eRk, encard_eq_zero]
  refine ⟨fun h ↦ by simpa [h] using! hI, fun h ↦ eq_empty_iff_forall_notMem.2 fun e heI ↦ ?_⟩
  exact (hI.indep.isNonloop_of_mem heI).not_isLoop (h (hI.subset heI))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard ≠ ⊤ ↔ M.RankFinite

Tactic:
encard_ne_top_iff

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.Finite ↔ M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_4
α : 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
⊢ ∀ (i : ι), z ∉ C i \ {x i}

Tactic:
simp only [mem_sdiff, mem_singleton_iff, not_and, not_not]

Goal state after:
case refine_4
α : 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
⊢ ∀ (i : ι), z ∈ C i → z = x i
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
⊢ I.encard = (f '' I).encard

Tactic:
hinj.encard_image

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
⊢ I.encard = I.encard
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) → e ∉ I

Tactic:
imp_not_comm

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M✶.closure (M✶.E \ B)

Tactic:
by rwa [hB'.closure_eq]

Goal state after:
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'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
⊢ (aeval (⇑f ∘ x✝)) x = (aeval (⇑f ∘ x✝)) y → x = y

Tactic:
hxy

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'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
hxy : (aeval (⇑f ∘ x✝)) x = (aeval (⇑f ∘ x✝)) y
⊢ x = y
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ J = I

Tactic:
rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]
  exact hI.subset.trans hJ

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
val✝ : ι'
⊢ (aeval (Sum.elim y x)) (X (Sum.inl val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inl val✝))

Tactic:
simp [e]

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
val✝ : ι
⊢ (aeval (Sum.elim y x)) (X (Sum.inr val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inr val✝))

Tactic:
simp [e]

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

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

Tactic:
or_iff_right (h.not_dep),

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.closure S ⊆ M.closure T

Tactic:
exact M.closure_subset_closure hST

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

Goal state before:
pp: case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
q : Subtype.val '' (fun i ↦ ⟨x i, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w

Tactic:
image_image

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
q : (fun x_1 ↦ ↑⟨x x_1, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ s

Tactic:
← eq

Goal state after:
case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ ↑S
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ finSepDegree F F = 1

Tactic:
by
  rw [finSepDegree, Nat.card_eq_one_iff_unique]
  constructor <;> infer_instance

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False

Tactic:
rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
      ← sub_pow_expChar] at hi

Goal state after:
case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hi : Irreducible ((X ^ q ^ n.pred - C z) ^ q)
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h.isOpen
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ IsOpen[inst✝³] (U ∩ U⁻¹)

pp: case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Tactic:
· exact Uopen.inter Uopen.inv

Goal state after:
case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h✝ : ExpChar F p
x : F
⊢ ∃ a, (frobenius F p) a = x

Tactic:
by
    obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'
    exact ⟨y, by rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy⟩

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
x : ↥(B.dualSubmodule N)
r : R
m : ↥N
⊢ (algebraMap R S) (B.dualSubmoduleParing x (r • m)) = (algebraMap R S) ((RingHom.id R) r • B.dualSubmoduleParing x m)

Tactic:
simp [← Algebra.smul_def]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
N : Submodule R M
r : R
x : ↥(B.dualSubmodule N)
y : ↥N
⊢ (algebraMap R S) ({ toFun := B.dualSubmoduleParing (r • x), map_add' := ⋯, map_smul' := ⋯ } y) =
    (algebraMap R S) (((RingHom.id R) r • { toFun := B.dualSubmoduleParing x, map_add' := ⋯, map_smul' := ⋯ }) y)

Tactic:
simp [← Algebra.smul_def]

Goal state after: