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

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
m : ℕ
z : K
hz : i z = y ^ p ^ m
⊢ (f.comp i) z = x ^ p ^ (n + m)

Tactic:
by rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

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

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep

Goal state after:
D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case neg
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)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ (X ^ n - C a).Separable

Tactic:
rw [← separable_map (algebraMap K K[n√a]), Polynomial.map_sub, Polynomial.map_pow, map_C, map_X,
    AdjoinRoot.algebraMap_eq,
    X_pow_sub_C_eq_prod (hζ.map_of_injective (algebraMap K _).injective) hn
    (root_X_pow_sub_C_pow n a), separable_prod_X_sub_C_iff']

Goal state after:
case neg
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)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ ∀ x ∈ Finset.range n,
    ∀ y ∈ Finset.range n,
      (algebraMap K K[n√a]) ζ ^ x * root (X ^ n - C a) = (algebraMap K K[n√a]) ζ ^ y * root (X ^ n - C a) → x = y
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ A.LinearDisjoint ⊥

Tactic:
by
  rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
  exact Submodule.LinearDisjoint.one_right _

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
this : Fintype ↑(Set.range p)
hcovers : ⋃ x ∈ (Set.range p).toFinset, ↑x = Set.univ
⊢ ∃ i, p i = ⊤

Tactic:
apply Set.mem_toFinset.mp (Subspace.top_mem_of_biUnion_eq_univ hcovers)

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
classical
  simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B)) x).det

Tactic:
Algebra.norm_eq_matrix_det (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B))) ((algebraMap (↥B) S) x)).det =
    (algebraMap R ↥A) ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B)) x).det
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
⊢ False

Tactic:
let := H.toField

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this : Field (A ⊗[R] B) := H.toField
⊢ False
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
⊢ False

Tactic:
obtain ⟨b, htb⟩ := ‹Algebra.Transcendental R B›

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
⊢ False
Module: Mathlib.RingTheory.LinearDisjoint

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

Tactic:
simp_rw [Algebra.smul_def, mul_one]; exact aeval_X _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

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

Tactic:
simp_rw [Algebra.smul_def, mul_one]; exact aeval_X _

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

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

Tactic:
algebraMap_elemReduct_eq,

Goal state after:
case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
⊢ (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
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✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective ⇑(algebraMap K L)
this : ExpChar L p
⊢ (algebraMap K L) (iterateFrobeniusAux K L p n (a + b)) = a ^ p ^ n + b ^ p ^ n

Tactic:
algebraMap_iterateFrobeniusAux K p hn (a + b),

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✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective ⇑(algebraMap K L)
this : ExpChar L p
⊢ (a + b) ^ p ^ n = a ^ p ^ n + b ^ p ^ n
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num).natDegree + (x * y).denom.natDegree

Tactic:
←
    Polynomial.natDegree_mul (mul_ne_zero (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy))
      (x * y).denom_ne_zero,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num * (x * y).denom).natDegree
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 v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ Module.rank F E * insepDegree E K = insepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_mul_lift_insepDegree_of_isPurelyInseparable F E K

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
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)
⊢ M ≤ restrictScalars F L

Tactic:
rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]

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)
⊢ M ≤ adjoin F (↑E' ∪ S)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ¬Φ' E = 0

Tactic:
exact Φ'_ne_zero h

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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

Tactic:
have := congr($(C_c_mul_φ h).coeff (φ E).natDegree)
  rw [coeff_C_mul, coeff_map, coeff_map, coeff_natDegree, IntermediateField.algebraMap_apply,
    φ_monic h, OneMemClass.coe_one, mul_one] at this
  exact this.symm

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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = (algebraMap K[X] K⟮X⟯) (c E).num

Tactic:
Φ_coeff_φ_natDegree h

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ c E = (algebraMap K[X] K⟮X⟯) (c E).num
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:
intro _

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✝ : M
⊢ ∀ {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
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:
intro _

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✝ : M
⊢ ∀ {y : M}, x✝ ∈ C → y ∈ C → x✝ + y ∈ ↑C.lineal → x✝ ∈ ↑C.lineal
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

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

Tactic:
intro _

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
a✝ : M
⊢ ∀ (b : N) (a : M) (b_1 : N) {a_1 : R},
    a✝ ∈ C₁ → b ∈ C₂ → a ∈ C₁ → b_1 ∈ C₂ → 0 < a_1 → a_1 • a✝ + a ∈ F₁ → a_1 • b + b_1 ∈ F₂ → a✝ ∈ F₁ ∧ b ∈ F₂
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
⊢ ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)

Tactic:
intro _

Goal state after:
X : Type u_1
d : DiffeologicalSpace X
t : TopologicalSpace X
h : dTopology = t
u✝ : Set X
⊢ TopologicalSpace.IsOpen u✝ ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u✝)
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x✝ : P
⊢ x✝ ∈
      mk' ((s.reindex e).points i) (affineSpan ℝ ((s.reindex e).points '' {i}ᶜ)).directionᗮ ⊓
        affineSpan ℝ (Set.range (s.reindex e).points) ↔
    x✝ ∈ (s.altitude ∘ ⇑e.symm) i

Tactic:
reindex_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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x✝ : P
⊢ x✝ ∈
      mk' ((s.points ∘ ⇑e.symm) i) (affineSpan ℝ ((fun a ↦ (s.points ∘ ⇑e.symm) a) '' {i}ᶜ)).directionᗮ ⊓
        affineSpan ℝ (Set.range (s.reindex e).points) ↔
    x✝ ∈ (s.altitude ∘ ⇑e.symm) i
Module: Mathlib.Geometry.Euclidean.Projection

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

Tactic:
←
      two_smul 𝕜 ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p),

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
h : 2 • (↑((orthogonalProjection s₁) p) -ᵥ ↑((orthogonalProjection s₂) p)) = 0
⊢ ↑((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
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₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f.toAffineMap p -ᵥ f.toAffineMap ↑((orthogonalProjection s) p) ∈
    (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ

Tactic:
← AffineMap.linearMap_vsub,

Goal state after:
𝕜 : 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₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f.linear (p -ᵥ ↑((orthogonalProjection s) p)) ∈ (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ
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
hwx : ℝ ∙ w = ℝ ∙ x
hyz : ℝ ∙ y = ℝ ∙ z
⊢ 2 • o.oangle w y = 2 • o.oangle x z

Tactic:
rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]

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₃ : P
r : ℝ
h : r ≠ 0
⊢ InnerProductGeometry.angle ((AffineMap.homothety p r) p₁ -ᵥ (AffineMap.homothety p r) p₂)
      ((AffineMap.homothety p r) p₃ -ᵥ (AffineMap.homothety p r) p₂) =
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
← AffineMap.linearMap_vsub,

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
r : ℝ
h : r ≠ 0
⊢ InnerProductGeometry.angle ((AffineMap.homothety p r).linear (p₁ -ᵥ p₂))
      ((AffineMap.homothety p r).linear (p₃ -ᵥ p₂)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
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.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
by_cases hx : ‖x‖ = 0

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
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₃ : P
r : ℝ
h : r ≠ 0
⊢ o.oangle ((AffineMap.homothety p r) p₁ -ᵥ (AffineMap.homothety p r) p₂)
      ((AffineMap.homothety p r) p₃ -ᵥ (AffineMap.homothety p r) p₂) =
    o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
← AffineMap.linearMap_vsub,

Goal state after:
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₃ : P
r : ℝ
h : r ≠ 0
⊢ o.oangle ((AffineMap.homothety p r).linear (p₁ -ᵥ p₂)) ((AffineMap.homothety p r).linear (p₃ -ᵥ p₂)) =
    o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π

Tactic:
have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy)

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‖
hy : y ≠ 0
hx : x ≠ 0
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = ↑π
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
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]

Goal state after:
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
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))

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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.kahler x) y ≠ 0
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
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)

Tactic:
← inner_neg_right

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)