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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
· rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]
    convert! Set.infinite_univ (α := Nat.Primes)
    rw [Set.eq_univ_iff_forall]
    intro ⟨p, hp⟩
    exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
⊢ ∃ s, IsTranscendenceBasis K Subtype.val

Tactic:
exact ⟨s, hs⟩

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

Goal state before:
pp: case succ
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
ih : ∀ {x : Extension k p n}, (frob k p n ^ i) x = x ^ Nat.card k ^ i
x : Extension k p n
⊢ (frob k p n) x ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)

Tactic:
frob_apply,

Goal state after:
case succ
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
i : ℕ
ih : ∀ {x : Extension k p n}, (frob k p n ^ i) x = x ^ Nat.card k ^ i
x : Extension k p n
⊢ (x ^ Nat.card k) ^ Nat.card k ^ i = x ^ Nat.card k ^ (i + 1)
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i ((M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec (fun x ↦ (algebraMap K L) (a x)) i) = i (0 i)

Tactic:
M,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i
      (((Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k).map
            ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec
        (fun x ↦ (algebraMap K L) (a x)) i) =
    i (0 i)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
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
h : i < ⊤
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne
      exact ⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (n, x) = mk K p (m + 1 + n, (⇑(frobenius K p))^[m + 1] x)

Tactic:
| succ m ih =>

Goal state after:
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) = toAlgEquivAux g x * toAlgEquivAux g y

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

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 * toAlgEquivAux g y
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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
⊢ ↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField) x) = ↑((↑g L) x)

Tactic:
have : ((limitToAlgEquiv g).restrictNormal L.unop) x = (limitToAlgEquiv g) x.1 := by
      exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x

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
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
this : ↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField) x) = (limitToAlgEquiv g) ↑x
⊢ ↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField) x) = ↑((↑g L) x)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : Relation.EqvGen (R K p) x y
⊢ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Tactic:
induction H with

Goal state after:
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
⊢ ⋃ 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:
have hD : D.FiniteIndex := finiteIndex_iInf' _ <| by simp

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
⊢ ⋃ 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.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
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))
this✝ : Algebra K K[n√a] := inferInstance
this : n ≠ 0
⊢ {root (X ^ n - C a)} ⊆ (X ^ n - C a).rootSet K[n√a]

Tactic:
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero
      (Nat.pos_of_ne_zero this) a), aeval_def, AdjoinRoot.algebraMap_eq, AdjoinRoot.eval₂_root]

Goal state after:
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
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
let E := F⟮a⟯ ⊔ F⟮b⟯
    have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)
    have : FiniteDimensional F F⟮b⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral b)
    have ha : a ∈ E := (le_sup_left : F⟮a⟯ ≤ E) <| mem_adjoin_simple_self F a
    have hb : b ∈ E := (le_sup_right : F⟮b⟯ ≤ E) <| mem_adjoin_simple_self F b
    have hab : a + b ∈ E := IntermediateField.add_mem E ha hb
    let a' : E := ⟨a, ha⟩
    let b' : E := ⟨b, hb⟩
    let ab' : E := ⟨a + b, hab⟩
    rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K b',
      normalizedTraceAux_intermediateField F K ab',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F b',
      normalizedTraceAux_eq_of_finiteDimensional F ab',
      ← smul_add, ← map_add, AddMemClass.mk_add_mk]

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
this : FiniteDimensional E ↥E⟮a⟯
⊢ (↑(Module.finrank E ↥E⟮a⟯) * ↑(Module.finrank F E))⁻¹ • (trace F E) ((trace E ↥E⟮a⟯) (AdjoinSimple.gen E a)) =
    (normalizedTrace F K) a

Tactic:
trace_trace,

Goal state after:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
this : FiniteDimensional E ↥E⟮a⟯
⊢ (↑(Module.finrank E ↥E⟮a⟯) * ↑(Module.finrank F E))⁻¹ • (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a) =
    (normalizedTrace F K) a
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
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ adjoin F S = adjoin F ((fun x ↦ x ^ q ^ n) '' S)

Tactic:
set M := adjoin F ((· ^ q ^ n) '' S)

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
⊢ adjoin F S = M
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this : ExpChar (↥M) q
⊢ (fun x ↦ x ^ q ^ n) '' S ⊆ ↑(adjoin F S)

Tactic:
rintro _ ⟨y, hy, rfl⟩
    exact pow_mem (subset_adjoin F S hy) _

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

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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
⊢ (Finsupp.linearCombination F fun x ↦ v x ^ q ^ n) lF₀ = 0

Tactic:
replace hl := congr($hl ^ q ^ n)

Goal state after:
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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : (Finsupp.linearCombination E v) l ^ q ^ n = 0 ^ q ^ n
⊢ (Finsupp.linearCombination F fun x ↦ v x ^ q ^ n) lF₀ = 0
Module: Mathlib.FieldTheory.RatFunc.Degree

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

Tactic:
sub_zero

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

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - 0 = ↑p.natDegree

Tactic:
sub_zero

Goal state after:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree = ↑p.natDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

Goal state after:
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
C D : PointedCone R N
hC : DualFG p C
hD : DualFG p D
⊢ DualFG p (C ⊓ D)

Tactic:
obtain ⟨S, rfl⟩ := hC

Goal state after:
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
D : PointedCone R N
hD : DualFG p D
S : Finset M
⊢ DualFG p (dual p ↑S ⊓ D)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

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 : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
x✝ y✝ : M
a : R
⊢ x✝ ∈ C → y✝ ∈ C → 0 < a → a • x✝ + y✝ ∈ C → (∀ p ∈ F, a • x✝ + y✝ ∈ p) → x✝ ∈ C ∧ ∀ p ∈ F, x✝ ∈ p

Tactic:
xc

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 : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
x✝ y✝ : M
a : R
xc : x✝ ∈ C
⊢ y✝ ∈ C → 0 < a → a • x✝ + y✝ ∈ C → (∀ p ∈ F, a • x✝ + y✝ ∈ p) → x✝ ∈ C ∧ ∀ p ∈ F, x✝ ∈ p
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
⊢ x✝ ∈ C → y✝ ∈ C → x✝ + y✝ ∈ ↑C.lineal → x✝ ∈ ↑C.lineal

Tactic:
xc

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
xc : x✝ ∈ C
⊢ y✝ ∈ C → x✝ + y✝ ∈ ↑C.lineal → x✝ ∈ ↑C.lineal
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
p₁ p₂ : P
inst✝¹ : Nonempty ↥s₁
inst✝ : s₁.direction.HasOrthogonalProjection
h : s₁ = s₂
hp : p₁ = p₂
⊢ ↑((orthogonalProjection s₁) p₁) = ↑((orthogonalProjection s₂) p₂)

Tactic:
subst h hp
  rfl

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

Goal state before:
pp: case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.height ((fun i ↦ i) ⟨1, ⋯⟩) = dist (s.points 0) (s.points 1)

Tactic:
dist_comm

Goal state after:
case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.height ((fun i ↦ i) ⟨1, ⋯⟩) = dist (s.points 1) (s.points 0)
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
θ : Real.Angle
⊢ (o.rotation θ) x = x ↔ x = 0 ∨ θ = 0

Tactic:
by_cases h : x = 0 <;> simp [h]

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 ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ

Tactic:
rw [← direction_affineSpan, ← 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.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)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
⊢ ∃ θ, f = o.rotation θ

Tactic:
by
  have : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
  obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
  use o.oangle x (f x)
  apply LinearIsometryEquiv.toLinearEquiv_injective
  apply LinearEquiv.toLinearMap_injective
  apply (o.basisRightAngleRotation x hx).ext
  intro i
  symm
  fin_cases i
  · simp
  have : o.oangle (J x) (f (J x)) = o.oangle x (f x) := by
    simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd,
      o.kahler_comp_rightAngleRotation]
  simp [← this]

Goal state after:
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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

pp: case p₃
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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ P

Tactic:
exact
    norm_sub_eq_abs_sub_norm_iff_angle_eq_zero (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he))
      fun he => hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
by
  rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [← neg_eq_zero] at h0
  rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]

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

Goal state before:
pp: case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 = 0
h1 : m 1 = 0
⊢ False

Tactic:
sub_zero

Goal state after:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ 0 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.SignedDist

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)
p : P
h : p ∈ affineSpan ℝ (Set.range s.points)
⊢ p ∈ affineSpan ℝ (insert (s.points i) (s.points '' {i}ᶜ))

Tactic:
convert! h

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
h : p ∈ affineSpan ℝ (Set.range s.points)
⊢ insert (s.points i) (s.points '' {i}ᶜ) = Set.range s.points
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
p q : P
hp : p ∈ s
hq : q ∈ s
hpq : p ≠ q
⊢ p ≠ s.center

Tactic:
grind [dist_eq_zero, mem_sphere']

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₂ s.center = s.radius

Tactic:
← mem_sphere.1 h.left_mem,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₂ s.center = dist p₁ s.center
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
← mem_sphere.1 h.left_mem,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * dist p₁ s.center
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
⊢ ↑((orthogonalProjection s₁) p) ≠ p' →
    ↑((orthogonalProjection s₂) p) ≠ p' →
      2 • ∡ (↑((orthogonalProjection s₁) p)) p' p = 2 • ∡ p p' ↑((orthogonalProjection s₂) p) →
        dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

Tactic:
by
  intro hp₁ hp₂ h
  have : Nonempty s₁ := ⟨p', hp'₁⟩
  have : Nonempty s₂ := ⟨p', hp'₂⟩
  have h' : ∡ (orthogonalProjection s₁ p : P) p' p = ∡ p p' (orthogonalProjection s₂ p) :=
    oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two h
      (angle_self_orthogonalProjection _ hp'₁) (angle_self_orthogonalProjection _ hp'₂)
  exact dist_orthogonalProjection_eq_of_oangle_eq hp'₁ hp'₂ hp₁ hp₂ h'

Goal state after: