mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑n

Tactic:
exact mod_cast h

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝ : NeZero f.natDegree
this : Fact (Irreducible f)
⊢ (aeval a) f = 0

Tactic:
aesop

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

Goal state before:
pp: case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this✝ : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : ↑((x.restrictNormal ↥L) y) = ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
exact SetLike.coe_eq_coe.mp this

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ ∃ n, i x ^ p ^ n = 0

Tactic:
exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩

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
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x = (((proj L) g).liftNormal K) x

Tactic:
toAlgEquivAux_eq_proj_of_mem g x L hx

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ ↑(((proj L) g) ⟨x, hx⟩) = (((proj L) g).liftNormal K) x
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : ¬IsSquare (-x)
⊢ IsSquare x

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : ¬IsSquare x
⊢ IsSquare (-x)

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
rcases exists_eq_pow_of_odd x (by simpa using hk) with ⟨r, hr⟩
    exact ⟨r⁻¹, by simpa using hr⟩

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case h.inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
even : Even n
⊢ ∃ r, x = r ^ n

Tactic:
rcases even with ⟨m, hm⟩
      rcases hx with ⟨s, hs⟩
      rcases isSquare_or_isSquare_neg s with (h | h) <;>
        rcases ih m (by lia) h (by lia) with ⟨r, hr⟩ <;>
        exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : IsRealClosed R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : 0 ≤ x
this : IsSquare (-x) → x = 0
⊢ IsSquare x

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
h : H.index > 0
⊢ H.index ≤ s.card

Tactic:
leftCoset_cover_const_iff_surjOn,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x ↦ ↑(g x)) (↑s) Set.univ
h : H.index > 0
⊢ H.index ≤ s.card
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Surjective fun x ↦ ↑(g ↑x)

Tactic:
leftCoset_cover_const_iff_surjOn,

Goal state after:
case left
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn (fun x ↦ ↑(g x)) (↑s) Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Surjective fun x ↦ ↑(g ↑x)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : n = 1
⊢ (X ^ n - C a).Separable

Tactic:
hn',

Goal state after:
case pos
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : n = 1
⊢ (X ^ 1 - C a).Separable
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
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
this : ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D

Tactic:
by
        have ⟨r, hr, hxr⟩ := this
        refine ⟨⟨⟨i, hi.1⟩, ⟨r, dif_pos hi.2 ▸ hr⟩⟩, rfl, ?_⟩
        simpa [K, f, if_pos hi.2] using! hxr

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
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
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
hk' : ∀ (i : ι), i ∈ s ∧ (H i).FiniteIndex → c ⊆ g i • ↑(H i) → ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
k₁ : κ
hik₁ : ↑k₁.fst = i
hk₁ : K k₁ = D
hxk₁ : x ∈ f k₁ • ↑D
k₂ : κ
hjk₂ : ↑k₂.fst = j
hk₂ : K k₂ = D
hxk₂ : x ∈ f k₂ • ↑D
⊢ x ∈ ⊥

Tactic:
rw [← Set.singleton_subset_iff] at hxk₁ hxk₂ ⊢

Goal state after:
case refine_3
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
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
hk' : ∀ (i : ι), i ∈ s ∧ (H i).FiniteIndex → c ⊆ g i • ↑(H i) → ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
k₁ : κ
hik₁ : ↑k₁.fst = i
hk₁ : K k₁ = D
hxk₁ : {x} ⊆ f k₁ • ↑D
k₂ : κ
hjk₂ : ↑k₂.fst = j
hk₂ : K k₂ = D
hxk₂ : {x} ⊆ f k₂ • ↑D
⊢ {x} ⊆ ⊥
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⋃ p ∈ s, ↑p = Set.univ
⊢ ⊤ ∈ s

Tactic:
by
  contrapose! hcovers
  exact Subspace.biUnion_ne_univ_of_top_notMem hcovers

Goal state after:
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
⊢ x✝ ∈ carrier 0 ↔ x✝ ∈ {0}

Tactic:
rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]

Goal state after:
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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ ∀ (x : ↥(perfectClosure F E)), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥(perfectClosure F E)).range

Tactic:
exact fun ⟨_, n, y, h⟩ ↦ ⟨n, y, (algebraMap _ E).injective h⟩

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ ((toSubmodule A').mulMap (toSubmodule B)) x' = ((toSubmodule A').mulMap (toSubmodule B)) y'

Tactic:
by simp [← Submodule.mulMap_comp_rTensor _ hA, hx', hy', hxy]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : Algebra.Transcendental K K⟮X⟯
⊢ False

Tactic:
Algebra.transcendental_iff_not_isAlgebraic

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : ¬Algebra.IsAlgebraic K K⟮X⟯
⊢ False
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relfinrank A = 1

Tactic:
by
  simp [relfinrank_eq_toNat_relrank]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
this : ∀ [inst : Field F] {x y : F⟮X⟯}, y ≠ 0 → x + y ≠ 0 → (x + y).intDegree ≤ max x.intDegree y.intDegree
⊢ (if x + y = 0 then 0 else exp (x + y).intDegree) ≤
    max (if x = 0 then 0 else exp x.intDegree) (if y = 0 then 0 else exp y.intDegree)

Tactic:
aesop

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
← Polynomial.map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E * φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_2
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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
hF :
  ∀ {x y : N} {a : R},
    ∀ x_1 ∈ C, f x_1 = x → ∀ x_2 ∈ C, f x_2 = y → 0 < a → ∀ x_3 ∈ F, f x_3 = a • x + y → ∃ x_4 ∈ F, f x_4 = x
w✝ : M
hx' : w✝ ∈ F
hhx' : f w✝ = f x✝
⊢ x✝ ∈ F

Tactic:
convert hx'

Goal state after:
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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
hF :
  ∀ {x y : N} {a : R},
    ∀ x_1 ∈ C, f x_1 = x → ∀ x_2 ∈ C, f x_2 = y → 0 < a → ∀ x_3 ∈ F, f x_3 = a • x + y → ∃ x_4 ∈ F, f x_4 = x
w✝ : M
hx' : w✝ ∈ F
hhx' : f w✝ = f x✝
⊢ x✝ = w✝
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
x' : EuclideanSpace ℝ (Fin n)
h : x' ∈ (OpenPartialHomeomorph.univBall x ε).source → ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ Metric.ball x ε
⊢ ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ u

Tactic:
aesop

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p

Tactic:
have h : d.isPlot (p ∘ OpenPartialHomeomorph.univBall x ε) := hu'
      (f := OpenPartialHomeomorph.univBall x ε)
      (fun x' ↦ by
        replace h := (OpenPartialHomeomorph.univBall x ε).map_source (x := x')
        rw [OpenPartialHomeomorph.univBall_target x hε] at h
        aesop)
      OpenPartialHomeomorph.contDiff_univBall

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)))
    ((Polynomial.mapRingHom (algebraMap K F)) (g E))

Tactic:
Associated.comm

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F)) (g E))
    ((Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)))
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace 𝕜 V
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ ↑((orthogonalProjection s₁) p) ∈ s₁.directionᗮ ⊓ s₂.directionᗮ

Tactic:
exact ⟨vsub_orthogonalProjection_mem_direction_orthogonal _ _,
    h ▸ vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩

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 : V
⊢ o.oangle x x = 0

Tactic:
rw [oangle, kahler_apply_self, ← ofReal_pow]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(↑(‖x‖ ^ 2)).arg = 0
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (s.restrict S hS).height i = s.height i

Tactic:
rw [eq_comm]
  convert! (s.restrict S hS).height_map S.subtypeₐᵢ i

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
v : V
hv : v ∈ s.direction
⊢ inner 𝕜 (f.linearIsometry.toLinearMap v) (f.linear (p -ᵥ ↑((orthogonalProjection s) p))) = 0

Tactic:
rw [AffineIsometry.linear_eq_linearIsometry, LinearIsometry.coe_toLinearMap,
    LinearIsometry.inner_map_map, Submodule.inner_right_of_mem_orthogonal hv
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V'
f : V ≃ₗᵢ[ℝ] V'
⊢ ((map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)

Tactic:
by
  simp [oangle, o.kahler_map]

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

Goal state before:
pp: case e'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = o.oangle (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)

pp: case e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃

Tactic:
· rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]

Goal state after:
case e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃