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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
induction hx using solvableByRad.induction with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
Function.leftInverse_iff_comp,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula = id
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
simp only [distinctConstantsTheory]

Goal state after:
L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    ⋃ t,
      (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
        (↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t) ∩
          (diagonal α)ᶜ)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
a✝ : α
⊢ Term.realize (⇑g ∘ v) (var a✝) = g (Term.realize v (var a✝))

pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))

Tactic:
· rfl

Goal state after:
case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Tactic:
subst h

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inr val✝)

Tactic:
· rfl

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_2
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⟩
⊢ (finRange φ_l).length ≤ φ_l

Tactic:
length_finRange

Goal state after:
case rel.refine_2
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⟩
⊢ φ_l ≤ φ_l
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ((sum fun i ↦ lift.{max u v, u} #(L.Functions i)) + sum fun i ↦ #(L.BoundedFormula Empty (i + 1))) =
    sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [add_comm, add_eq_max, max_eq_left]

Goal state after:
L : Language
⊢ (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'

Tactic:
refine
    ⟨elementarySkolem₁Reduct (closure (L.sum L.skolem₁) (s ∪ Equiv.ulift '' s')),
      (s.subset_union_left).trans subset_closure, ?_⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)

Tactic:
apply Monotone.directed_le
    refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
    simp only [Finset.coe_map, Function.Embedding.coe_subtype]
    exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
      Set.monotone_image fun _ _ => Finset.coe_subset.2

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
⊢ Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)

Tactic:
Algebra.isAlgebraic_iff_isIntegral,

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
⊢ Algebra.IsIntegral k (MvPolynomial σ k ⧸ I)
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
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K := fun s ↦ φ ((Ideal.Quotient.mk I) (X s))
⊢ ∃ x, I = vanishingIdeal k {x}

Tactic:
have : aeval x = φ.comp (Quotient.mkₐ k I) := by ext; simp [x]

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)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K := fun s ↦ φ ((Ideal.Quotient.mk I) (X s))
this : aeval x = φ.comp (Quotient.mkₐ k I)
⊢ ∃ x, I = vanishingIdeal k {x}
Module: Mathlib.FieldTheory.Finite.Polynomial

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

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 [map_add]; intro _ _ hf hg; rw [hf, hg]

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 * X n) = (expand p) (p_1 * X n)
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, (MvPolynomial.eval c) M.det = 1

Tactic:
by
    obtain ⟨g, hg⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp
      (hq ▸ Submodule.mem_top (x := Pi.single 1 1))
    simp_rw [RingHom.map_det]
    refine ⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩
    ext i j
    simpa [M, Pi.single_apply, inv_mul_eq_one, mul_comm, Matrix.one_apply]
      using! congr($hg (i⁻¹ * j))

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: 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 : (Module.rank F E).ord.ToType
⊢ adjoin F (⇑b ∘ φ '' Iio (i⁺)) = IntermediateField.restrictScalars F (↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯

Tactic:
by
  rw [Iio_succ, ← Iio_insert, image_insert_eq, ← union_singleton, adjoin_adjoin_left]; rfl

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: 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
f : ↥(filtration (i⁺)) →ₐ[F] Ē
⊢ ((equivSucc i) f).1 = embFunctor F E ⋯ f

Tactic:
cases i; exacts [rfl, succEquiv_coherence _ f]

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i ↦ #(Cardinal.factor ↑i)) ≤ 2 ^ Module.rank F E

Tactic:
rw [← power_eq_two_power rank_inf natCast_le_aleph0 rank_inf]

Goal state after:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i ↦ #(Cardinal.factor ↑i)) ≤ ℵ₀ ^ Module.rank F E
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
⊢ ∃ m, 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0

Tactic:
obtain ⟨m, hm⟩ := exists_pow_mem_center_of_inseparable' p ha hinsep

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
⊢ ∃ m, 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
⊢ elemExponent K a ≤ n

Tactic:
let ⟨p, _⟩ := ExpChar.exists K

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
⊢ elemExponent K a ≤ n
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: 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
⊢ HasExponent K L

Tactic:
let ⟨p, _⟩ := ExpChar.exists K

Goal state after:
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
⊢ HasExponent K L
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : K
⊢ (algebraMap K L) ((iterateFrobenius K L p hn) ((algebraMap K L) a)) = (algebraMap K L) (a ^ p ^ n)

Tactic:
rw [map_pow, algebraMap_iterateFrobenius K p hn]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
c : K
⊢ Module.finrank (↥K⟮C c⟯) K⟮X⟯ = max (C c).num.natDegree (C c).denom.natDegree

Tactic:
adjoin_simple_eq_bot_iff.mpr (show C c ∈ ⊥ from ⟨c, rfl⟩),

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
c : K
⊢ Module.finrank (↥⊥) K⟮X⟯ = max (C c).num.natDegree (C c).denom.natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ generator E ∉ (algebraMap K K⟮X⟯).range

Tactic:
rw [generator_eq_coeff h]
  intro ⟨f, hf⟩
  exact (exists_φ_coeff_not_mem h).choose_spec ⟨f, by ext; exact hf⟩

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 (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
classical
  rw [map_mul, mul_assoc]
  conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]
  rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]
  · rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
    exact Φ'_ne_zero h

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ f '' s ⊆ (convexHull R) (f '' s) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s

Tactic:
(IsConvexSet.convexHull.image hf).convexHull_subset_iff

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ f '' s ⊆ (convexHull R) (f '' s) ∧ f '' s ⊆ f '' (convexHull R) s
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
h : s = s'
p : P
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s') p)

Tactic:
subst h

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s) 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 s' : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : s.direction.HasOrthogonalProjection
inst✝ : s'.direction.HasOrthogonalProjection
h : s = s'
p : P
⊢ (reflection s) p = (reflection s') p

Tactic:
subst h

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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
⊢ (reflection s) p = (reflection s) p
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

Tactic:
by
  rintro rfl; simp at h

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

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

Tactic:
by
  rintro rfl; simp at h

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

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

Tactic:
by
  rintro rfl; simp at 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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h : ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i)) = s.points i
⊢ False

Tactic:
orthogonalProjectionSpan,

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)
h : ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i)) = s.points i
⊢ False
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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
⊢ ↑((orthogonalProjection (affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points))) (f p)) =
    f ↑((orthogonalProjection (affineSpan 𝕜 (Set.range s.points))) p)

Tactic:
convert! orthogonalProjection_map (affineSpan 𝕜 (Set.range s.points)) f p

Goal state after:
case h
𝕜 : 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₂
n : ℕ
s : Simplex 𝕜 P n
f : P →ᵃⁱ[𝕜] P₂
p : P
⊢ affineSpan 𝕜 (Set.range (s.map f.toAffineMap ⋯).points) =
    AffineSubspace.map f.toAffineMap (affineSpan 𝕜 (Set.range s.points))
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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂

Tactic:
rw [add_smul, ← neg_vsub_eq_vsub_rev p₂ p₃, smul_neg, neg_smul, ← hpr]

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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ - -(p₄ -ᵥ p₃) + 1 • -(p₂ -ᵥ p₃) = p₄ -ᵥ p₂
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₃ = 0
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
  exact norm_sub_eq_abs_sub_norm_of_angle_eq_zero h

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle y x + (o.oangle x (x - y) + o.oangle (y - x) y) = ↑π

Tactic:
← oangle_neg_neg,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle (-y) (-x) + (o.oangle x (x - y) + o.oangle (y - x) y) = ↑π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑(2 * π) = 0

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0

Tactic:
Real.Angle.coe_two_pi

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ 0 = 0

V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂

Tactic:
by
  have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]

Goal state after: