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

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

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

Tactic:
· simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]

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

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
⊢ N ⊨ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩
  contrapose h
  rw [← Sentence.realize_not] at *
  exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)

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
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L ((insert i s).inf f)

Tactic:
rw [Finset.inf_insert]

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L (f i ⊓ s.inf f)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
simp only [Formula.realize_iExs, Formula.realize_inf, Formula.realize_iAlls, Formula.realize_imp,
    Formula.realize_relabel]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (∃ i,
      φ.Realize (Sum.elim v i) ∧
        ∀ (i_1 : γ → M),
          φ.Realize ((fun a ↦ Sum.elim (Sum.elim v i) i_1 a) ∘ fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) →
            Formula.Realize (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g)))) fun a ↦
              Sum.elim (Sum.elim v i) i_1 a) ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max u v w, w} κ ≤ #↑N

Tactic:
refine _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) ?_

Goal state after:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
this : ↑N ⊨ L.distinctConstantsTheory Set.univ
⊢ lift.{max (max u v) w, w} #(Quotient.out κ) ≤ #↑N
Module: Mathlib.ModelTheory.Skolem

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

Tactic:
refine _root_.trans ?_ (lift_le.2 (mk_le_mk_of_subset Set.subset_union_right))
    rw [aleph0_le_lift, ← aleph0_le_lift, h]
    exact h1

Goal state after:
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: case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]

Goal state after:
case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ ¬CharP K p
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : ℕ
h✝ : ¬ℵ₀ ≤ ↑a
x✝ : ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
n : ℕ
han : ↑a = ↑n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
h : p ^ k = n
⊢ ↑p ^ k = ↑a

Tactic:
rw [han]; exact mod_cast h

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

Goal state before:
pp: case inr.inl.refine_1
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ (Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X)).Splits

pp: case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0

Tactic:
· apply IsSplittingField.splits

Goal state after:
case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑a

pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
· simp [mul_comm]

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ x = r ^ n

Tactic:
by linear_combination - (by simpa using hr : r ^ n - x = 0)

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
D : Subgroup G := ⋯
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) := ⋯
f : κ → G := ⋯
K : κ → Subgroup G := ⋯
⊢ ⋃ x ∈ {k | (H ↑k.fst).FiniteIndex}, f x • ↑(K x) = ⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • ↑(H x)

Tactic:
rw [Set.iUnion_sigma, Set.iUnion_subtype]

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
⊢ ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {k | (H ↑k.fst).FiniteIndex}), f ⟨⟨x, hx⟩, a⟩ • ↑(K ⟨⟨x, hx⟩, a⟩) =
    ⋃ x ∈ {i ∈ s | (H i).FiniteIndex}, g x • ↑(H x)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
D : Subgroup G := ⋯
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) := ⋯
f : κ → G := ⋯
K : κ → Subgroup G := ⋯
⊢ ⋃ x ∈ {a | ¬(H ↑a.fst).FiniteIndex}, f x • ↑(K x) = ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • ↑(H x)

Tactic:
rw [Set.iUnion_sigma, Set.iUnion_subtype]

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
⊢ ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨x, hx⟩, a⟩ • ↑(K ⟨⟨x, hx⟩, a⟩) =
    ⋃ x ∈ {a ∈ s | ¬(H a).FiniteIndex}, g x • ↑(H x)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_1
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)⁻¹
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ

Tactic:
rw [← hcovers', Set.iUnion_sigma, Set.iUnion_subtype]

Goal state after:
case refine_1
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)⁻¹
⊢ ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) =
    ⋃ x, ⋃ (hx : x ∈ s), ⋃ a, ⋃ (_ : ⟨⟨x, hx⟩, a⟩ ∈ {x | K x = D}), f ⟨⟨x, hx⟩, a⟩ • ↑D
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ α ^ finrank K L - (algebraMap K L) a = 0

Tactic:
ha,

Goal state after:
case adjoin_rootSet'
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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ (algebraMap K L) a - (algebraMap K L) a = 0
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A.toSubalgebra ⊔ B.toSubalgebra) = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra

Tactic:
← sup_toSubalgebra_of_left

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A ⊔ B).toSubalgebra = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: 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 ⊗[R] ↥⊥ ≃ₐ[R] ↥A

Tactic:
refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).rTensorOne ?_ ?_

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₁ a₂ : ↥A) (b₁ b₂ : ↥⊥),
    (toSubmodule A).rTensorOne ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (toSubmodule A).rTensorOne (a₁ ⊗ₜ[R] b₁) * (toSubmodule A).rTensorOne (a₂ ⊗ₜ[R] b₂)

case refine_2
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
⊢ (toSubmodule A).rTensorOne (1 ⊗ₜ[R] 1) = 1
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥L' ↑A).toSubsemiring

Tactic:
adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ (Algebra.adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥L' ↑A).toSubsemiring
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥A ↑L').toSubsemiring

Tactic:
adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
⊢ (Algebra.adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥A ↑L').toSubsemiring
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✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime (finrank R ↥B)
⊢ A.LinearDisjoint B

Tactic:
by
  nontriviality R
  by_cases h1 : Module.finrank R A = 0
  · rw [h1, Nat.coprime_zero_left] at H
    rw [eq_bot_of_finrank_one H]
    exact bot_right _
  by_cases h2 : Module.finrank R B = 0
  · rw [h2, Nat.coprime_zero_right] at H
    rw [eq_bot_of_finrank_one H]
    exact bot_left _
  have := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h1)
  have := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h2)
  have := finite_sup A B
  have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
    LinearMap.finrank_le_finrank_of_injective <|
      Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)
  exact of_finrank_sup_of_free <| (finrank_sup_le_of_free A B).antisymm <|
    Nat.le_of_dvd (lt_of_lt_of_le (Nat.pos_of_ne_zero h1) this) <| H.mul_dvd_of_dvd_of_dvd
      (finrank_left_dvd_finrank_sup_of_free A B) (finrank_right_dvd_finrank_sup_of_free A B)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
C : PointedCone R N
hC : DualFG p C
⊢ DualFG LinearMap.id C

Tactic:
obtain ⟨s, rfl⟩ := hC
  use Finset.image p s
  simp

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ A.relrank ⊤ = A.relrank ⊤ * Module.rank (↥⊤) E

Tactic:
IntermediateField.rank_top,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ A.relrank ⊤ = A.relrank ⊤ * 1
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case refine_3
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (vectorSpan ℝ ((s.map f.toAffineMap ⋯).points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points) =
    Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓
      Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (Set.range s.points))

Tactic:
Submodule.map_orthogonal,

Goal state after:
case refine_3
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (vectorSpan ℝ ((s.map f.toAffineMap ⋯).points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points) =
    (Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ f.linearIsometry.range ⊓
      Submodule.map f.linearIsometry.toLinearMap (vectorSpan ℝ (Set.range s.points))
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
⊢ 2 • o.oangle x (-y) = 2 • o.oangle x y

Tactic:
by_cases hy : y = 0
    · simp [hy]
    · simp [o.oangle_neg_right hx hy]

Goal state after: