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

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ (Formula.graph f).Realize (Fin.cons (funMap f x) x)
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_1
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  (List.map Sum.getLeft?
            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
    true
h2 :
  (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ cast ⋯
      (((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l))[i]?.bind id).get ⋯).snd =
    ts i

Tactic:
rw [cast_eq_iff_heq]

Goal state after:
case rel.refine_1
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  (List.map Sum.getLeft?
            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
    true
h2 :
  (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ (((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l))[i]?.bind id).get ⋯).snd ≍ ts i
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
hD : A.Definable₁ L D
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ A
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
V : Set (σ → K)
p q : MvPolynomial σ k
hq : q ∈ {p | ∀ x ∈ V, (aeval x) p = 0}
x : σ → K
hx : x ∈ V
⊢ (aeval x) (p • q) = 0

Tactic:
by
    simp only [hq x hx, smul_eq_mul, mul_zero, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ ∃ x, I = vanishingIdeal k {x}

Tactic:
have : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I) := by
    rw [Algebra.isAlgebraic_iff_isIntegral, ← algebraMap_isIntegral_iff]
    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this✝ : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
⊢ ∃ x, I = vanishingIdeal k {x}
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

Tactic:
rwa [mul_comm] at hbc

Goal state after:
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:
simpa using ax_grothendieck_zeroLocus 0 p

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

Goal state before:
pp: F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ ((algebraMap F K) a)′ / (algebraMap F K) a = (algebraMap F K) (a′ / a)

Tactic:
simp [deriv_algebraMap]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
⊢ ∀ (x : F[X]),
    (AdjoinRoot.mk p).toIntAlgHom x = 0 →
      (AdjoinRoot.mk p).toIntAlgHom
          ((implicitDeriv
              ((AdjoinRoot.modByMonicHom ⋯)
                (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
            x) =
        0

Tactic:
rintro x hx

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
x : F[X]
hx : (AdjoinRoot.mk p).toIntAlgHom x = 0
⊢ (AdjoinRoot.mk p).toIntAlgHom
      ((implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯)
            (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
        x) =
    0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = (expand p) (p_1 * X n)

Tactic:
simp only [expand_X, map_mul]

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) p_1 * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p_1 * X n ^ p
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
⊢ mk K p (n, 0) = 0

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [← ih]
    apply (Quot.sound _).symm
    have := R.intro (p := p) n (0 : K)
    rwa [map_zero] at this

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : CommSemiring K
inst✝² : CommSemiring L
i : K →+* L
p : ℕ
inst✝¹ : ExpChar L p
inst✝ : PerfectRing L p
x : K
h : x ∈ pNilradical K p
⊢ x ∈ ker i

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 h
  replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))
  rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h

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
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (Quot.mk (R K p) (m, x) + Quot.mk (R K p) (n, y)) * Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) * Quot.mk (R K p) (s, z) + Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z)

Tactic:
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_assoc, add_comm _ s,
              add_left_comm _ s]
            apply R.sound
            simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply,
              add_mul, add_comm, add_left_comm]

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
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : j y = x ^ p ^ n
⊢ (equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)

Tactic:
by
  rw [equiv_symm, equiv_apply j i p _ _ _ h]

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
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
normalizedTraceAux_intermediateField F K 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
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b
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
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F K a

Tactic:
normalizedTraceAux_intermediateField F K 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
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F (↥E) a'
Module: Mathlib.FieldTheory.PrimeField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
⊢ (algebraMap ℚ K).fieldRange = ⊥

Tactic:
eq_bot_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
⊢ (algebraMap ℚ K).fieldRange ≤ ⊥
Module: Mathlib.FieldTheory.PrimeField

Goal state before:
pp: K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
⊢ (algebraMap (ZMod p) K).fieldRange = ⊥

Tactic:
eq_bot_iff,

Goal state after:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
⊢ (algebraMap (ZMod p) K).fieldRange ≤ ⊥
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
⊢ IsPurelyInseparable F ↥(adjoin F S) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by
  simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
⊢ M = ⊥

Tactic:
let : Field K := Ideal.Quotient.field _

Goal state after:
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
⊢ M = ⊥
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Polynomial.C f.num - Polynomial.C f.denom * Polynomial.X = Polynomial.C f.num + Polynomial.C (-f.denom) * Polynomial.X

Tactic:
map_neg,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Polynomial.C f.num - Polynomial.C f.denom * Polynomial.X = Polynomial.C f.num + -Polynomial.C f.denom * Polynomial.X
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 : Fin (n + 1)
⊢ (mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),

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 : Fin (n + 1)
⊢ (mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ).direction ⊓
      (affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
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 : Fin (n + 1)
⊢ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ (affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
direction_affineSpan,

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 : Fin (n + 1)
⊢ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ (affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
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)
p : P
⊢ line[ℝ, p, s.points i].direction = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ (affineSpan ℝ (Set.range s.points)).direction ∧
        p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
direction_affineSpan,

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
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ (affineSpan ℝ (Set.range s.points)).direction ∧
        p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ
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)
p : P
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ (affineSpan ℝ (Set.range s.points)).direction ∧
        p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
direction_affineSpan,

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
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧
        p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).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 : ∠ p₁ p₂ p₃ = π
heq : dist p₁ p₂ = 0
⊢ False

Tactic:
dist_eq_zero

Goal state after:
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 : ∠ p₁ p₂ p₃ = π
heq : p₁ = p₂
⊢ False
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
⊢ ⟪x, (o.rotation ↑(π / 2)) x⟫ = 0

Tactic:
rw [real_inner_comm, inner_rotation_pi_div_two_left]

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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑π

Tactic:
rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx,
    show o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) =
      o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) by abel,
    o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add]

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

Goal state before:
pp: case refine_2.inr.inr.inl.inr
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 : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rw [Set.insert_comm, Set.pair_comm]
        exact h.collinear

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃

Tactic:
simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, oangle]
  convert! o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq _ h using 1
  · rw [← neg_vsub_eq_vsub_rev p₁ p₃, ← neg_vsub_eq_vsub_rev p₁ p₂, o.oangle_neg_neg]
  · rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]; simp
  · simpa using hn

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ : P
h : (∡ p₁ p p₂).sign = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π

Tactic:
convert! o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h <;> simp

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

Goal state before:
pp: case refine_1
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 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + 0 * r = 0
h1 : m 1 = 0
⊢ False

Tactic:
rw [zero_mul, add_zero] at h0

Goal state after:
case refine_1
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 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 = 0
h1 : m 1 = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
s : Set (V × V) := (fun r' ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (fun z ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ ↑π
hx : (x, y) ∈ s
hy : (x, r • x + y) ∈ s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
convert! Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy

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

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
⊢ (mk' (midpoint ℝ p₁ p₂) ((innerₛₗ ℝ) (p₂ -ᵥ p₁)).ker).direction = (ℝ ∙ (p₂ -ᵥ p₁))ᗮ

Tactic:
direction_mk'

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ ((innerₛₗ ℝ) (p₂ -ᵥ p₁)).ker = (ℝ ∙ (p₂ -ᵥ p₁))ᗮ
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p : P
⊢ (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ).direction = (ℝ ∙ (p -ᵥ s.center))ᗮ

Tactic:
direction_mk'

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
⊢ (ℝ ∙ (p -ᵥ s.center))ᗮ = (ℝ ∙ (p -ᵥ s.center))ᗮ