mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      ((algebraMap ↥L ↥L')
        ((((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ })
                g).restrictNormal
            ↥L)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
AlgEquiv.restrictNormal_commutes (proj (mk L') g) L

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g)
        ((algebraMap ↥L
            ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional✝,
                  isGalois := isGalois✝ }.toIntermediateField)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
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 y : K
hx : x ∈ (adjoin k {x, y}).toIntermediateField
hy : y ∈ (adjoin k {x, y}).toIntermediateField
⊢ toAlgEquivAux g (x * y) = (((proj (adjoin k {x, y})) g).liftNormal K) x * toAlgEquivAux g y

Tactic:
toAlgEquivAux_eq_liftNormal g y (adjoin k {x, y}) hy,

Goal state after:
k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
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 y : K
hx : x ∈ (adjoin k {x, y}).toIntermediateField
hy : y ∈ (adjoin k {x, y}).toIntermediateField
⊢ toAlgEquivAux g (x * y) =
    (((proj (adjoin k {x, y})) g).liftNormal K) x * (((proj (adjoin k {x, y})) g).liftNormal K) y
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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.index ≤ s.card

Tactic:
cases H.index.eq_zero_or_pos with
  | inl h => exact h ▸ s.card.zero_le
  | inr h =>
    rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
    exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
k : κ
this : ↑k.1 ∈ s ∧ H ↑k.1 ≠ H j
⊢ K k ∈ (Finset.image H s).erase (H j)

Tactic:
exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s.erase i, m x * ∏ x ∈ s.erase x, (i - x) + m i * ∏ x ∈ s.erase i, (i - x) = 0
⊢ m i = 0

Tactic:
Finset.sum_eq_zero h2,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : 0 + m i * ∏ x ∈ s.erase i, (i - x) = 0
⊢ m i = 0
Module: Mathlib.RingTheory.TensorProduct.Nontrivial

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
this : IsDomain R
⊢ Nontrivial (A ⊗[R] B)

Tactic:
let FR := FractionRing R

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
this : IsDomain R
FR : Type u_1 := FractionRing R
⊢ Nontrivial (A ⊗[R] B)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : (Submodule.mulLeftMap (toSubmodule B) a).ker = ⊥
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
mulLeftMap_ker_eq_bot_iff_linearIndependent_op

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
x✝ : L
⊢ (map (algebraMap K L) (mk K x✝).minpoly).Splits

Tactic:
minpoly_mk

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
x✝ : L
⊢ (map (algebraMap K L) (minpoly K x✝)).Splits
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (mk K x✝).minpoly.Monic

Tactic:
minpoly_mk

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (minpoly K x✝).Monic
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (mk K x✝).minpoly

Tactic:
minpoly_mk

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (minpoly K x✝)
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
have ha : a ∈ E := (le_sup_left : F⟮a⟯ ≤ E) <| mem_adjoin_simple_self F a

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝³ : Field (A ⊗[R] B) := H.toField
a : A
b : B
htb : Transcendental R b
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝² : IsDomain A
this✝¹ : IsDomain B
this✝ : IsDomain R
this : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
⊢ False

Tactic:
replace htb : Function.Injective gb := transcendental_iff_injective.1 htb

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝³ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝² : IsDomain A
this✝¹ : IsDomain B
this✝ : IsDomain R
this : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
⊢ False
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ (algebraMap K L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e

Tactic:
rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound a)]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case h
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 : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ x⁻¹ ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS

Tactic:
rw [inv_pow]

Goal state after:
case h
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 : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ (x ^ ringExpChar F ^ n)⁻¹ ∈ (algebraMap F E).rangeS
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 n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
rw [linearIndependent_iff_finset_linearIndependent] at h ⊢

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
⊢ ∀ (s : Finset ι), LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ ↑0 - ↑(natDegree 1) = 0

Tactic:
natDegree_one,

Goal state after:
K : Type u
inst✝ : Field K
⊢ ↑0 - ↑0 = 0
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
k : K
⊢ ↑0 - ↑(natDegree 1) = 0

Tactic:
natDegree_one,

Goal state after:
K : Type u
inst✝ : Field K
k : K
⊢ ↑0 - ↑0 = 0
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ DualFG p (dual p ↑(Submodule.span { c // 0 ≤ c } ↑s))

Tactic:
use s

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ dual p ↑s = dual p ↑(Submodule.span { c // 0 ≤ c } ↑s)
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Finset M
⊢ DualFG p (dual p ↑s)

Tactic:
use s

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ (aeval X) ((generator E).minpolyX ↥K⟮generator E⟯) = 0

Tactic:
exact (generator E).minpolyX_aeval_X

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

Goal state before:
pp: case refine_1
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 : Function.Surjective ⇑f
hc : (comap f F).IsFaceOf (comap f C)
x : M
xF : x ∈ F
⊢ x ∈ C

Tactic:
rw [← (hf x).choose_spec] at xF ⊢
    exact mem_comap.mp (hc.1 xF)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
a✝² : M
b✝¹ : N
a✝¹ : M
b✝ : N
a✝ : R
xc₁ : a✝² ∈ C₁
⊢ b✝¹ ∈ C₂ → a✝¹ ∈ C₁ → b✝ ∈ C₂ → 0 < a✝ → a✝ • a✝² + a✝¹ ∈ F₁ → a✝ • b✝¹ + b✝ ∈ F₂ → a✝² ∈ F₁ ∧ b✝¹ ∈ F₂

Tactic:
xc₂

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
a✝² : M
b✝¹ : N
a✝¹ : M
b✝ : N
a✝ : R
xc₁ : a✝² ∈ C₁
xc₂ : b✝¹ ∈ C₂
⊢ a✝¹ ∈ C₁ → b✝ ∈ C₂ → 0 < a✝ → a✝ • a✝² + a✝¹ ∈ F₁ → a✝ • b✝¹ + b✝ ∈ F₂ → a✝² ∈ F₁ ∧ b✝¹ ∈ 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 : (Polynomial.C (Polynomial.C (Q₃ h)) * Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Φ E)).natDegree = (θ E).natDegree

Tactic:
natDegree_mul (C_ne_zero.mpr (Q₃_map h ▸ Q₂_ne_zero h))
      ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Φ_ne_zero h)),

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (Polynomial.C (Polynomial.C (Q₃ h))).natDegree + (Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Φ E)).natDegree = (θ E).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ E = K⟮generator E⟯

pp: case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ E = K⟮generator E⟯

Tactic:
· rwa [generator_eq_zero h, adjoin_zero]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ E = K⟮generator E⟯
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mp
𝕜 : 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 : AffineSubspace 𝕜 P
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty ↥s
h : p₂ = ↑((orthogonalProjection s) p₁) ∨ p₂ = ↑((orthogonalProjection s) p₁)
⊢ ↑((orthogonalProjection s) p₁) = p₂

Tactic:
or_self,

Goal state after:
case mp
𝕜 : 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 : AffineSubspace 𝕜 P
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty ↥s
h : p₂ = ↑((orthogonalProjection s) p₁)
⊢ ↑((orthogonalProjection s) p₁) = p₂
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 : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑⟨p, hp⟩ -ᵥ (v +ᵥ p)) +ᵥ ↑⟨p, hp⟩ = -v +ᵥ p

Tactic:
vsub_vadd_eq_vsub_sub

Goal state after:
𝕜 : 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 : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑⟨p, hp⟩ -ᵥ p - v) +ᵥ ↑⟨p, hp⟩ = -v +ᵥ p
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
θ : Real.Angle
⊢ o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hx : x = 0
  · simp [hx, eq_comm]
  · by_cases hy : y = 0
    · simp [hy, eq_comm]
    · rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
      simp [hx, hy]

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

Goal state before:
pp: case a.refine_2
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range s.points))ᗮ

Tactic:
rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]

Goal state after:
case a.refine_2
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ ∧
    s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
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 : V
⊢ ⟪(o.rotation ↑(π / 2)) x, x⟫ = 0

Tactic:
by
  rw [rotation_pi_div_two, inner_rightAngleRotation_self]

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 : V
r : ℝ
⊢ ⟪(o.rotation ↑(π / 2)) x, r • x⟫ = 0

Tactic:
by
  rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]

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

Goal state before:
pp: case neg.mpr.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
H : x ≠ 0 ∧ 0 • (o.rotation ↑(π / 2)) x ≠ 0
⊢ (∃ r, 0 < r ∧ 0 • (o.rotation ↑(π / 2)) x = r • (o.rotation ↑(π / 2)) x) ∨
    ∃ r, 0 < r ∧ 0 • (o.rotation ↑(π / 2)) x = -r • (o.rotation ↑(π / 2)) x

pp: case neg.mpr.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
hr0 : r < 0
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x

Tactic:
· simp_all

Goal state after:
case neg.mpr.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
hr0 : r < 0
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x