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

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ (⇑hnp ∘ ⇑hmn ∘ x✝) ↔ RelMap r✝ x✝

Tactic:
map_rel,

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ (⇑hmn ∘ x✝) ↔ RelMap r✝ x✝
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2
L : Language
α : Type u'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
· rw [max_le_iff, ← infinite_iff]
    refine ⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩
    · cases ij
      rfl
    · rw [Cardinal.le_def]
      refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩
      rintro (a | a) (b | b) h
      · simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h
        rw [h]
      · simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h
        rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
ι : Type u_2
inst✝ : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
⊢ A.Definable L (⋃ i, f i)

Tactic:
have := Fintype.ofFinite ι
  convert! definable_finset_sup hf Finset.univ using 1
  simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ A.Definable L {v | f v = g v}

Tactic:
have hF : A.DefinableMap L (fun v => ![f v, g v]) := by
    simp [DefinableMap, *]
  exact (Definable.diagonal L A).preimage_map hF

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
p : ℕ
hp : p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
subst hp
    let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
    exact ⟨⟨AlgebraicClosure ℚ⟩⟩

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
refine ⟨⟨∅, ?_⟩⟩

Goal state after:
case inl
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∀ q ∉ ∅, Theory.ACF ↑q ⊨ᵇ ψ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
simp only [hφn, true_iff]
    intro hφ
    rw [models_sentence_iff] at *
    exact hφn h.1.some (hφ _)

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ ↦ ↑(f ↑φ ⋯)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
⊢ p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
hpψ

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ ↦ ↑(f ↑φ ⋯)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : p ∉ s
⊢ Theory.ACF ↑p ⊨ᵇ ψ
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s, (Fintype.card K - 1) • {s}

Tactic:
refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ∪ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ IsNoetherian K (R σ K)

Tactic:
IsNoetherian.iff_rank_lt_aleph0

Goal state after:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.rank K (R σ K) < ℵ₀
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
h : x ∈ Ideal.comap i (pNilradical L p)
⊢ ∃ n, x ^ p ^ n = 0

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h
    obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)
    exact ⟨n + m, by rwa [pow_add, pow_mul]⟩

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
n : ℕ
h : x ^ p ^ n = 0
⊢ x ∈ ker i

Tactic:
replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))

Goal state after:
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
n : ℕ
h : (iterateFrobeniusEquiv L p n).symm (i (x ^ p ^ n)) = (iterateFrobeniusEquiv L p n).symm (i 0)
⊢ x ∈ ker i
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = (↑(H ↑i).index)⁻¹ * ↑(D.relIndex (H ↑i) * (H ↑i).index)

Tactic:
Nat.cast_mul,

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
i : ↥s
x✝ : i ∈ s.attach
hfi : (H ↑i).FiniteIndex
⊢ ∑ s_1, ↑(if K ⟨i, s_1⟩ = D then 1 else 0) = (↑(H ↑i).index)⁻¹ * (↑(D.relIndex (H ↑i)) * ↑(H ↑i).index)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
hq' : (aeval α) q = 0
⊢ (X ^ finrank K L - C a).degree ≤ (minpoly K α).degree

Tactic:
rw [degree_X_pow_sub_C finrank_pos,
        degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)),
        ← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]

Goal state after:
case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
hq' : (aeval α) q = 0
⊢ finrank K L ≤ finrank K ↥⊤
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✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ normalizedTraceAux F K a =
    ↑(Module.finrank (↥F⟮a⟯) K) * (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a) /
      ↑(Module.finrank F ↥F⟮a⟯ * Module.finrank (↥F⟮a⟯) K)

Tactic:
Nat.cast_mul,

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✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ normalizedTraceAux F K a =
    ↑(Module.finrank (↥F⟮a⟯) K) * (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a) /
      (↑(Module.finrank F ↥F⟮a⟯) * ↑(Module.finrank (↥F⟮a⟯) K))
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R S) x' = ↑x
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)

Tactic:
replace hx : algebraMap R _ x' = x := Subtype.val_injective hx

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥) x' = x
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R S) x' = ↑x
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)

Tactic:
replace hx : algebraMap R _ x' = x := Subtype.val_injective hx

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)
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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
⊢ sepDegree E ↥(adjoin E S) = sepDegree F ↥M

Tactic:
set L := adjoin E S

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
⊢ sepDegree E ↥L = sepDegree F ↥M
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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝ : Algebra ↥M ↥L := i.toAlgebra
this : SMul ↥M ↥L := this✝.toSMul
⊢ sepDegree E ↥L = sepDegree F ↥M

Tactic:
have : IsScalarTower F M L := IsScalarTower.of_algebraMap_eq (congrFun rfl)

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝¹ : Algebra ↥M ↥L := i.toAlgebra
this✝ : SMul ↥M ↥L := this✝¹.toSMul
this : IsScalarTower F ↥M ↥L
⊢ sepDegree E ↥L = sepDegree F ↥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
this✝ : UniqueFactorizationMonoid ↥K[f]
H : (f.minpolyX ↥K[f]).natDegree = 0
this : (f.minpolyX ↥K⟮f⟯).natDegree = 0
⊢ False

Tactic:
f.natDegree_minpolyX,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this✝ : UniqueFactorizationMonoid ↥K[f]
H : (f.minpolyX ↥K[f]).natDegree = 0
this : max f.num.natDegree f.denom.natDegree = 0
⊢ False
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)
⊢ vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
exact (Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left

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

Goal state before:
pp: case mpr
𝕜 : 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 q : P
⊢ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ → ↑((orthogonalProjection s) p) = q

Tactic:
rintro ⟨hqs, hpq⟩
    have hq : q ∈ mk' p s.directionᗮ := by
      rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
    suffices q ∈ ({(orthogonalProjection s p : P)} : Set P) by
      simpa [eq_comm] using this
    rw [← inter_eq_singleton_orthogonalProjection]
    simp only [Set.mem_inter_iff, SetLike.mem_coe]
    exact ⟨hqs, hq⟩

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)
θ : Real.Angle
x✝ : V
⊢ (o.rotation θ).symm x✝ = (o.rotation (-θ)) x✝

Tactic:
simp [o.rotation_apply, o.rotation_symm_apply, sub_eq_add_neg]

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

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

Tactic:
by
  rw [reflection_apply', reflection_apply']
  constructor
  · intro h
    rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
      vsub_sub_vsub_cancel_right, ←
      two_smul 𝕜 ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p), smul_eq_zero] at h
    simpa using h
  · intro h
    rw [h]

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

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

Tactic:
rw [o.eq_iff_oangle_eq_zero_of_norm_eq]

Goal state after:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ ‖(o.rotation (o.oangle x y)) x‖ = ‖y‖
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
obtain rfl | hij := eq_or_ne i j
  · rw [real_inner_self_eq_norm_sq]
    refine lt_of_lt_of_le (b := 0) ?_ ?_
    · rw [neg_lt_zero]
      positivity
    · positivity
  rw [neg_lt]
  refine lt_of_abs_lt ?_
  rw [abs_neg]
  exact abs_inner_vsub_altitudeFoot_lt_mul s hij

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
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h,
    Real.arccos_eq_arcsin (div_nonneg (norm_nonneg _) (norm_nonneg _)), div_pow, one_sub_div hxy]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin √((‖x + y‖ ^ 2 - ‖x‖ ^ 2) / ‖x + y‖ ^ 2) = Real.arcsin (‖y‖ / ‖x + y‖)
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
⊢ Real.sin (angle x (x + -y)) * ‖x + -y‖ = ‖y‖

Tactic:
sin_angle_add_mul_norm_of_inner_eq_zero h,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ ‖-y‖ = ‖y‖
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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z

Tactic:
by
  refine ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => ?_⟩
  rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, h]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
  exact angle_add_le_pi_div_two_of_inner_eq_zero h

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 : ℝ
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
r' : ℝ
hz : x = 0
⊢ False

Tactic:
simpa [hz] using (h' 0).1

Goal state after:
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)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
    angle_eq_arccos_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]

Goal state after:
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)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs,
    angle_eq_arctan_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (right_ne_of_oangle_eq_pi_div_two h)]

Goal state after:
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)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂

Tactic:
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:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝¹ : MetricSpace E
inst✝ : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
p : E
hp : p ∈ ps
⊢ dist (f p) (f c) = r

Tactic:
rw [hf.dist_eq, hc p hp]

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

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
hr : s.center ∈ s
hm : s.center ∈ as
⊢ s.radius = 0 ∧ s.center ∈ as

Tactic:
center_mem_iff

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ s.radius = 0 ∧ s.center ∈ as