mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
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
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
j : ι
hj : j ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
⊢ x ∈ c → x ∈ ⊥

Tactic:
hx

Goal state after:
case refine_3
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
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
j : ι
hj : j ∈ {x | x ∈ s ∧ (H x).FiniteIndex}
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.LinearDisjoint

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

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

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
s : Finset (Subspace k E)
hcovers : ⋃ p ∈ s, ↑p = Set.univ
⊢ ⊤ ∈ s

Tactic:
contrapose! hcovers

Goal state after:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⊤ ∉ s
⊢ ⋃ p ∈ s, ↑p ≠ Set.univ
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
x : L
⊢ mk K x = 0 ↔ x = 0

Tactic:
by
  rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Field S
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra K S
inst✝⁴ : Algebra L S
inst✝³ : IsScalarTower K L S
inst✝² : Normal K L
inst✝¹ : DecidableEq L
inst✝ : Fintype Gal(L/K)
c : ConjRootClass K L
x x✝ : L
⊢ x✝ ∈ Finset.image (fun x_1 ↦ x_1 x) Finset.univ ↔ x✝ ∈ carrier ⟦x⟧

Tactic:
simp [← isConjRoot_iff_exists_algEquiv, ← mk_eq_mk]

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
n : Normal K L
c : ConjRootClass K L
⊢ (map (algebraMap K L) c.minpoly).Splits

Tactic:
by
  induction c
  rw [minpoly_mk]
  exact n.splits _

Goal state after:
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
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
⊢ fa a = a ⊗ₜ[R] 1

Tactic:
simp [fa]

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

Goal state before:
pp: case prime
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
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ elemExponent K a ≤ n

Tactic:
obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h
    let f := X ^ ringExpChar K ^ n - C y
    have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
    have hf₂ : f.Monic := monic_X_pow_sub_C y <| Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K _ _
    have hf₃ : f.natDegree = ringExpChar K ^ n := by
      rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
    exact (Nat.pow_le_pow_iff_right <| Nat.Prime.one_lt hp).mp <|
      ringExpChar.eq K p ▸ hf₃ ▸ minpoly_natDegree_eq K a ▸
      natDegree_le_natDegree (minpoly.min K a hf₂ hf₁)

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
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R ↥A * finrank R ↥B
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Tactic:
← Module.finrank_tensorProduct

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R (↥A ⊗[R] ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B
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
x : E
⊢ x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

Tactic:
by
  rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]

Goal state after:
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
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
⊢ x ∈ L → x ∈ perfectClosure F E

Tactic:
hx

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range
x : E
hx : x ∈ L
⊢ x ∈ perfectClosure F E
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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = x' ^ p ^ (n + 1)
⊢ ⟨x' ^ p, ⋯⟩ = x

Tactic:
hx

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
h : lF₀ = 0
⊢ l i = 0 i

Tactic:
refine eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
h : lF₀ = 0
⊢ (algebraMap F E) (lF i) = 0
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
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ f * ↑this.unit = minpoly F x

Tactic:
IsUnit.unit_spec,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ f * C f.leadingCoeff⁻¹ = minpoly F x
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le h]
  let : Algebra A B := (inclusion h).toAlgebra
  have : IsScalarTower A B E := IsScalarTower.of_algebraMap_eq' rfl
  exact rank_mul_rank A B E

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ A ⊓ f.fieldRange ⊓ (B ⊓ f.fieldRange) = A ⊓ (B ⊓ f.fieldRange)

Tactic:
rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y

Tactic:
by
  rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
  by_cases hx : x = 0
  · rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
  · by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
    · simp_all [RatFunc.intDegree_mul]

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 ≠ ⊥
⊢ (Φ E).coeff (generatorIndex h) ≠ 0

Tactic:
by
  apply_fun algebraMap K[X] K⟮X⟯
  rw [map_zero, Φ_coeff_generatorIndex h]
  exact mul_ne_zero_iff.mpr ⟨algebraMap_ne_zero (num_ne_zero (c_ne_zero h)), generator_ne_zero h⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case le
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x : M
⊢ x ∈ map (LinearMap.fst R M N) F → x ∈ C₁

Tactic:
hx

Goal state after:
case le
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x : M
hx : x ∈ map (LinearMap.fst R M N) F
⊢ x ∈ C₁
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
⊢ x ∈ C₁ → y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F

Tactic:
hx

Goal state after:
case mem_of_smul_add_mem
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
hx : x ∈ C₁
⊢ y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: case e_dTopology
X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝¹ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₁ n
plot_reparam✝¹ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₁ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₁ n
locality✝¹ :
  ∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
    (∀ (x : EuclideanSpace ℝ (Fin n)),
        ∃ u,
          IsOpen u ∧
            x ∈ u ∧
              ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ p₁ m) →
      p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₂ n
plot_reparam✝ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₂ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₂ n
locality✝ :
  ∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
    (∀ (x : EuclideanSpace ℝ (Fin n)),
        ∃ u,
          IsOpen u ∧
            x ∈ u ∧
              ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ p₂ m) →
      p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  @IsPlot X
      { plots := p₁, constant_plots := constant_plots✝¹, plot_reparam := plot_reparam✝¹, locality := locality✝¹,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ } =
    @IsPlot X
      { plots := p₂, constant_plots := constant_plots✝, plot_reparam := plot_reparam✝, locality := locality✝,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ }
s : Set X
⊢ IsOpen[t₁] s ↔ IsOpen[t₂] s

Tactic:
exact ((show p₁ = p₂ from h) ▸ @h₁ s).trans (@h₂ s).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 ≠ ⊥
⊢ (Φ E).natDegree = (θ E).natDegree

Tactic:
have := congr($(Q₂_mul_Φ h).natDegree)
  rwa [natDegree_mul (Polynomial.map_ne_zero (Q₂_ne_zero h)) (Φ_ne_zero h), natDegree_map,
    Q₂_natDegree h, zero_add] at this

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', direction_affineSpan, direction_affineSpan]

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 : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
⊢ ↑((orthogonalProjection s) p) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ

Tactic:
constructor
  · rintro rfl
    exact ⟨orthogonalProjection_mem _, vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩
  · 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.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
r : ℝ
hr : r < 0
⊢ o.oangle x (r • y) = o.oangle x (-y)

Tactic:
by
  rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)]

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

Goal state before:
pp: case a
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)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠
    dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)

Tactic:
dist_eq_norm_vsub

Goal state after:
case a
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)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠
    ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)

Tactic:
refine ⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, ?_⟩

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑π

Tactic:
by
  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.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h0 : ¬x = 0
h : ⟪x, y⟫ = 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (√(‖x‖ ^ 2) * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Tactic:
← Real.sqrt_mul (sq_nonneg _)

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h0 : ¬x = 0
h : ⟪x, y⟫ = 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / √(‖x‖ ^ 2 * (1 + (‖y‖ / ‖x‖) ^ 2)))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mpr
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₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ → ∠ p₁ p₂ p₃ = 0

Tactic:
· rintro (⟨hp₁p₂, h⟩ | ⟨hp₃p₂, h⟩)
    · exact h.angle₂₁₃_eq_zero_of_ne hp₁p₂
    · exact h.angle₃₁₂_eq_zero_of_ne hp₃p₂

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

Goal state before:
pp: case neg
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
hx : x = r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)
⊢ (-o).oangle (r • ((-o).rotation (-↑(π / 2))) x) (r • ((-o).rotation (-↑(π / 2))) x + x) = ↑(Real.arctan r⁻¹)

Tactic:
hx

Goal state after:
case neg
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
hx : x = r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)
⊢ (-o).oangle (r • ((-o).rotation (-↑(π / 2))) x)
      (r • ((-o).rotation (-↑(π / 2))) x + r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)) =
    ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case neg
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
hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))
⊢ o.oangle (-(r • (o.rotation ↑(π / 2)) x) + x) x = ↑(Real.arctan r)

Tactic:
hx

Goal state after:
case neg
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
hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))
⊢ o.oangle (-(r • (o.rotation ↑(π / 2)) x) + x) (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case neg
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
hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))
⊢ o.oangle (-(r • (o.rotation ↑(π / 2)) x) + x) (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)

Tactic:
hx

Goal state after:
case neg
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
hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))
⊢ o.oangle (-(r • (o.rotation ↑(π / 2)) x) + r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x)))
      (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)