mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ castAdd 0) ∘ Sum.inl ∘ g) (default ∘ natAdd 0) ↔
    BoundedFormula.Realize φ (v ∘ g) default

Tactic:
iff_eq_eq,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ castAdd 0) ∘ Sum.inl ∘ g) (default ∘ natAdd 0) =
    BoundedFormula.Realize φ (v ∘ g) default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst✝ : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iInf f).Realize v v' ↔ ∀ (b : β), (f b).Realize v v'

Tactic:
by
  simp only [iInf, realize_foldr_inf, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
    forall_exists_index, forall_apply_eq_imp_iff]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ BoundedFormula.Realize φ (⇑g ∘ v) default ↔ BoundedFormula.Realize φ (⇑g ∘ v) (⇑g ∘ default)

Tactic:
iff_eq_eq,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ BoundedFormula.Realize φ (⇑g ∘ v) default = BoundedFormula.Realize φ (⇑g ∘ v) (⇑g ∘ default)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst✝ : DecidablePred p
hp : A.Definable L (ofPred p)
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ DefinableFun L A fun v ↦ if p v then f v else g v

Tactic:
let P : Set (Option α → M) := {w | p (w ∘ some)}
  have hP : A.Definable L P := hp.preimage_comp some
  simp only [DefinableFun]
  convert! (hP.inter hf).union (hP.compl.inter hg)
  ext w
  by_cases h : p (w ∘ some) <;> simp [tupleGraph, P, h]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
h₂ : ∀ {n : ℕ} (g : L[[↑A]].Functions n), A.TermDefinable L' fun v ↦ Term.realize v g.term
x : L[[↑A]].Term β
⊢ A.TermDefinable L' fun v ↦ Term.realize v x

Tactic:
choose c hc using @h₂

Goal state after:
M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
x : L[[↑A]].Term β
c : {n : ℕ} → L[[↑A]].Functions n → L'[[↑A]].Term (Fin n)
hc : ∀ {n : ℕ} (g : L[[↑A]].Functions n), (fun v ↦ Term.realize v g.term) = fun v ↦ Term.realize v (c g)
⊢ A.TermDefinable L' fun v ↦ Term.realize v x
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀

Tactic:
rw [rank_subsingleton]

Goal state after:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ 1 ≤ max #↑s ℵ₀
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
this : ∀ (i j : ℕ), i ≠ j → s ^ i = s ^ j → j < i → ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
hlt : i ≤ j
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
· exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
this : ∀ (i j : ℕ), i ≠ j → s ^ i • x = s ^ j • x → j < i → ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
hlt : i ≤ j
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
· exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Goal state after:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := ⋯
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := ⋯
res : ↑S' → ↑S' := ⋯
x y : ↑S'
hxy : res x = res y
i : ι
⊢ ↑(↑x i) = ↑(↑y i)

Tactic:
simp only [Subtype.ext_iff, funext_iff] at hxy

Goal state after:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
x y : ↑S'
i : ι
hxy : ∀ (x_1 : ι), ↑(↑(res x) x_1) = ↑(↑(res y) x_1)
⊢ ↑(↑x i) = ↑(↑y i)
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
⊢ (Function.Injective fun v i ↦ (eval v) (p i)) → Function.Surjective fun v i ↦ (eval v) (p i)

Tactic:
by
  simpa using ax_grothendieck_zeroLocus 0 p

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ y, ∑ x, ↑(c x) * logDeriv (y (u x)) + ∑ x, (x v)′

Tactic:
← sum_add_distrib

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
x✝ : b (φ j) ∈ adjoin F (⇑b ∘ φ '' Iio i)
⊢ Iio i ⊆ Iio j

Tactic:
exact fun k (hk : k < i) ↦ hk.trans h

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : Nonempty ↑(Iio i)
⊢ (fun f ↦ Subalgebra.iSupLift (fun x ↦ ((fun j ↦ filtration ↑j) x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯)
      ((fun f ↦ ⟨fun j ↦ embFunctor F E ⋯ f, ⋯⟩) f) =
    f

Tactic:
ext ⟨x, hx⟩
      rw [← iSup_filtration hi, mem_toSubalgebra, ← SetLike.mem_coe,
          coe_iSup_of_directed directed_filtration, mem_iUnion] at hx
      rw [Subalgebra.iSupLift_of_mem _ _ (by exact hx.choose_spec)]; rfl

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).1, -(n, x).2) ((n + 1, (frobenius K p) x).1, -(n + 1, (frobenius K p) x).2)

Tactic:
rw [← map_neg]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).1, -(n, x).2) ((n + 1, (frobenius K p) x).1, (frobenius K p) (-x))
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ liftAux (RingHom.id K) j p x = j x

Tactic:
rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f ↦ f.comp i) f = (fun f ↦ f.comp i) g
⊢ f = g

Tactic:
ext x
  obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x
  apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n
  simpa only [← map_pow, ← hx] using! congr($(heq) y)

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
A : Set Gal(K/k)
⊢ A ∈ 𝓝 1 ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Tactic:
rw [krullTopology_mem_nhds_one_iff_of_normal]
  exact ⟨fun ⟨L, _, hL, hsub⟩ ↦ ⟨{ toIntermediateField := L, isGalois := ⟨⟩ }, hsub⟩,
    fun ⟨L, hL⟩ ↦ ⟨L, inferInstance, inferInstance, hL⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ (taylor r) p ∈ R[X]⁰

Tactic:
rw [mem_nonZeroDivisors_iff_right]

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
⊢ ∀ (x : R[X]), x * (taylor r) p = 0 → x = 0
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i ↦ g i • ↑(H i))

Tactic:
replace hcovers' : ⋃ i ∈ Finset.univ.filter (K · = D), f i • (D : Set G) = Set.univ := by
    rw [← hk, Set.iUnion₂_congr fun i hi => by rw [← (Finset.mem_filter.mp hi).2]]
    by_contra! h
    obtain ⟨i, -, hi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers' k (Finset.mem_univ k) h
    by_cases hfi : (H i.1.1).FiniteIndex <;> simp [K, hfi, hkfi] at hi

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
    1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
      (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i ↦ g i • ↑(H i))
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ mk K 0 = mk K x ↔ x = 0

Tactic:
mk_eq_mk,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ IsConjRoot K 0 x ↔ x = 0
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a b : L
h : a + b = 0
⊢ mk K a = mk K (-b)

Tactic:
mk_eq_mk,

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a b : L
h : a + b = 0
⊢ IsConjRoot K a (-b)
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars ⋯) * Module.rank (↥(adjoin L ↑A)) E) =
    Cardinal.lift.{w, v} (Module.rank (↥A) E)

Tactic:
Cardinal.lift_inj

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars ⋯) * Module.rank (↥(adjoin L ↑A)) E = Module.rank (↥A) E
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
S : Set E
⊢ adjoin F S ≤ perfectClosure F E ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
adjoin_le_iff,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
S : Set E
⊢ S ⊆ ↑(perfectClosure F E) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  rw [intDegree_add hxy, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
    mul_comm y.denom, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
    le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ←
    le_max_iff, mul_comm y.num]
  exact natDegree_add_le _ _

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
h : F.IsFaceOf C
⊢ ∀ ⦃x : M⦄, x ∈ ↑C → ∀ ⦃y : M⦄, y ∈ ↑C → ∀ ⦃z : M⦄, z ∈ ↑F → z ∈ openSegment R x y → x ∈ ↑F

Tactic:
rintro _ xc _ yc _ zf ⟨_, _, a0, b0, -, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
h : F.IsFaceOf C
x✝ : M
xc : x✝ ∈ ↑C
y✝ : M
yc : y✝ ∈ ↑C
w✝¹ w✝ : R
a0 : 0 < w✝¹
b0 : 0 < w✝
zf : w✝¹ • x✝ + w✝ • y✝ ∈ ↑F
⊢ x✝ ∈ ↑F
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
| (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)

Tactic:
enter [2, 1, 2]; rw [← num_div_denom (generator E)]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) * (algebraMap K[X] K⟮X⟯) (g E) =
    (algebraMap K[X] K⟮X⟯) (c E).num * generator E * (algebraMap K[X] K⟮X⟯) (g E)
| (algebraMap K[X] K⟮X⟯) (generator E).num / (algebraMap K[X] K⟮X⟯) (generator E).denom
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hF : F.IsFaceOf C
⊢ (comap f F).IsFaceOf (comap f C)

Tactic:
refine ⟨comap_mono hF.le, ?_⟩
  simp only [mem_comap, map_add, map_smul]
  exact hF.mem_of_smul_add_mem

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ finrank ℝ ↥(s.altitude i).direction = 1

Tactic:
by
  rw [direction_altitude]
  have h := Submodule.finrank_add_inf_finrank_orthogonal
    (vectorSpan_mono ℝ (Set.image_subset_range s.points {i}ᶜ))
  have hn : (n - 1) + 1 = n := by
    have := NeZero.ne n
    cases n <;> lia
  have hc : #({i}ᶜ) = (n - 1) + 1 := by
    rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]
  refine add_left_cancel (_root_.trans h ?_)
  classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rw [Matrix.toLin_self]
    simp [rotation_apply, Fin.sum_univ_succ]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  · by_cases hy : y = 0
    · simp [hy]
    · simp [o.oangle_neg_left hx hy]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle y ((o.rotation (o.oangle x y)) x) = 0

Tactic:
by
  rw [oangle_rev]
  simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ s.points i -ᵥ s.altitudeFoot i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
← Affine.Simplex.range_faceOpposite_points

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ s.points i -ᵥ s.altitudeFoot i ∈ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).directionᗮ
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ False

Tactic:
exact Real.pi_ne_zero (by linarith)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
rw [← neg_smul]

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)