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

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑s

Tactic:
rw [Set.iUnion_eq_iUnion_finset] at hs

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ¬↑M ⊨ φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
rw [← Sentence.realize_not] at h

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
exact Model.isSatisfiable M

Goal state after:
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
g : Gal(Extension k p n/k)
⊢ ∃ i < n, frob k p n ^ i = g

Tactic:
let := Fintype.ofFinite k

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
g : Gal(Extension k p n/k)
this : Fintype k := Fintype.ofFinite k
⊢ ∃ i < n, frob k p n ^ i = g
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p (n2 + n1)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
iterateFrobeniusEquiv_symm_add_apply,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm (j y1) *
      (iterateFrobeniusEquiv M p n2).symm ((iterateFrobeniusEquiv M p n1).symm (j y2 ^ p ^ n1)) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2) = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
add_pow_expChar_pow

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

Tactic:
natCast K p 0,

Goal state after:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : mk K p (0, ↑x) = ↑y
⊢ ↑x = ↑y
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : mk K p (0, ↑x) = ↑y
⊢ ↑x = ↑y

Tactic:
natCast K p 0,

Goal state after:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : mk K p (0, ↑x) = mk K p (0, ↑y)
⊢ ↑x = ↑y
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

Tactic:
natCast K p 0,

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ mk K p (0, ↑x) = ↑y
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ mk K p (0, ↑x) = ↑y

Tactic:
natCast K p 0,

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ mk K p (0, ↑x) = mk K p (0, ↑y)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p (n2 + n1)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
iterateFrobeniusEquiv_symm_add_apply,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm (j y1) +
      (iterateFrobeniusEquiv M p n2).symm ((iterateFrobeniusEquiv M p n1).symm (j y2 ^ p ^ n1)) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: 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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
i : κ
hi : i ∈ {x | K x = K k}
⊢ f i • ↑(K k) = ?m.488 i hi

Tactic:
← (Finset.mem_filter.mp hi).2

Goal state after:
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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
i : κ
hi : i ∈ {x | K x = K k}
⊢ f i • ↑(K i) = ?m.488 i hi
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case neg
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) = (↑0)⁻¹ * ↑D.index

Tactic:
Nat.cast_zero,

Goal state after:
case neg
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) = 0⁻¹ * ↑D.index
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
have : IsRoot (minpoly K σ.toLinearMap) ζ := by
    rw [IsGalois.card_aut_eq_finrank] at hσ'
    simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ',
      sub_eq_zero] using hζ.pow_eq_one

Goal state after:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inl
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ (↑0)⁻¹ < (↑s.card)⁻¹

Tactic:
Nat.cast_zero,

Goal state after:
case inl
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ 0⁻¹ < (↑s.card)⁻¹
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥A = 1

Tactic:
← inf_of_le_left (le_refl A)

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ A) = 1
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 K)

Tactic:
← Module.finrank_mul_finrank F F⟮a⟯ K,

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.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
⊢ f (fb b) = f (a ⊗ₜ[R] 1)

Tactic:
simp_rw [fb, Algebra.TensorProduct.includeRight_apply, f,
      Algebra.TensorProduct.mapOfCompatibleSMul_tmul]

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
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
⊢ 1 ⊗ₜ[R[X]] b = a ⊗ₜ[R[X]] 1
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range
n : ℕ
y : F
h : (algebraMap F K) y = i x ^ ringExpChar F ^ n
⊢ i ((algebraMap F E) y) = i (x ^ ringExpChar F ^ n)

Tactic:
AlgHom.commutes,

Goal state after:
case refine_1
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range
n : ℕ
y : F
h : (algebraMap F K) y = i x ^ ringExpChar F ^ n
⊢ (algebraMap F K) y = i (x ^ ringExpChar F ^ n)
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
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x

Tactic:
obtain ⟨x', hx⟩ := surjective_frobenius E p x.1

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
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : (frobenius E p) x' = ↑x
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p).intDegree = ↑p.natDegree

Tactic:
by
  rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
⊢ A = ⊥

Tactic:
← inf_of_le_left (le_refl A)

Goal state after:
R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
⊢ A ⊓ A = ⊥
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Q₂ h ≠ 0

Tactic:
by
  apply_fun Polynomial.map Polynomial.C
  rw [Polynomial.map_zero, Q₂_map]
  exact Q₁_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 ≠ ⊥
H : ¬(Q₂ h).natDegree = 0
F : Type u_1 := AlgebraicClosure K
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0

Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero.not, ← degree_map _ (algebraMap K F)] at H

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
⊢ (generator E).num.natDegree = 0 ∧ (generator E).denom.natDegree = 0
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : DiffeologicalSpace X
inst✝ : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ Continuous[dTopology, dTopology] f

Tactic:
continuous_def,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : DiffeologicalSpace X
inst✝ : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ ∀ (s : Set Y), IsOpen[dTopology] s → IsOpen[dTopology] (f ⁻¹' s)
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 : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
⊢ (s.reindex e).height i = (s.height ∘ ⇑e.symm) i

Tactic:
simp [height]

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
V₂ : Type u_3
P₂ : Type u_4
inst✝⁴ : NormedAddCommGroup V₂
inst✝³ : InnerProductSpace ℝ V₂
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).height i = s.height i

Tactic:
simp [height]

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)
⊢ 0 < s.height i

Tactic:
simp [height]

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

Goal state before:
pp: case «0»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.height ((fun i ↦ i) ⟨0, ⋯⟩) = dist (s.points 0) (s.points 1)

Tactic:
simp [height]

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

Goal state before:
pp: case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.height ((fun i ↦ i) ⟨1, ⋯⟩) = dist (s.points 1) (s.points 0)

Tactic:
simp [height]

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
⊢ o.oangle x y = 0 ↔ SameRay ℝ x y

Tactic:
by
  rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
    Complex.arg_eq_zero_iff]
  simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y

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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (fun y ↦ ∠ y.1 y.2.1 y.2.2) x

Tactic:
let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
  have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
  have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
  exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp (by fun_prop)

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ 0 < |s.height i * s.height j|

Tactic:
simp [height]

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✝ : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ 0 < s.height i * s.height j

Tactic:
simp [height]

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

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

Tactic:
by
  simp_rw [oangle]
  rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]
  · congr 1
    exact mod_cast Complex.arg_real_mul _ (by positivity : 0 < ‖y‖ ^ 2)
  · exact o.kahler_ne_zero hx hy
  · exact o.kahler_ne_zero hy hz

Goal state after: