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

Goal state before:
pp: case rel.hc
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
⊢ ((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
        ⋯).fst =
    ⟨φ_n, rel φ_R ts⟩.fst

Tactic:
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)

Goal state after:
case rel.hc
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  (List.map Sum.getLeft?
            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
    true
h2 :
  (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ ((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
        ⋯).fst =
    ⟨φ_n, rel φ_R ts⟩.fst
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_1
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
⊢ cast ⋯
      (((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l))[i]?.bind id).get ⋯).snd =
    ts i

Tactic:
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)

Goal state after:
case rel.refine_1
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  (List.map Sum.getLeft?
            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
    true
h2 :
  (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ cast ⋯
      (((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l))[i]?.bind id).get ⋯).snd =
    ts i
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝³ : L.Structure M
α : Type u'
inst✝² : DecidableEq α
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
h : M ⊨ equivSentence φ
⊢ M ⊨ φ.exClosure

Tactic:
by
  rw [Formula.realize_exClosure]
  exists fun a => (L.con (a : α) : M)
  simpa [Formula.Realize, BoundedFormula.realize_restrictFreeVar] using h

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

Goal state before:
pp: p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
⊢ κ.Categorical (Theory.ACF p)

Tactic:
rintro ⟨M⟩ ⟨N⟩ hM hN

Goal state after:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
⊢ Nonempty
    (↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } ≃[Language.ring]
      ↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ })
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
C : L[[↑A]].Constants
⊢ Function.const (α → M) ↑C = fun v ↦ Term.realize v C.term

Tactic:
by simp only [Term.realize_constants]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
⊢ ↑M ⊨ Formula.equivSentence φ

Tactic:
let := (L.lhomWithConstants α).reduct M

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ ↑M ⊨ Formula.equivSentence φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
constructor
  · intro hcomp
    refine ⟨hcomp.1, ?_⟩
    intro M N
    rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
  · rintro ⟨hsat, h⟩
    refine ⟨hsat, ?_⟩
    intro φ
    obtain ⟨M⟩ := hsat
    by_cases hφ : M ⊨ φ
    · left
      exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ
    · right
      exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst✝⁵ : L.Structure M
inst✝⁴ : L.Structure N
inst✝³ : M ⊨ T
inst✝² : N ⊨ T
inst✝¹ : Nonempty M
inst✝ : Nonempty N
⊢ M ≅[L] N

Tactic:
by
  rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : AlgebraicIndependent K x
⊢ Finite ι

Tactic:
by
  rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0]
  exact hx.lift_cardinalMk_le_trdeg.trans_lt (Cardinal.lift_lt_aleph0.mpr (trdeg_lt_aleph0 K L))

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case a
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
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
x : ι
| logDeriv ↑(u x)

Tactic:
apply logDeriv_algebraMap (u x)

Goal state after:
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ {y}
⊢ False

Tactic:
(isClopen_discrete _).eq_univ <| singleton_nonempty y

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
let M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial _ L) :=
    .of fun i j ↦ ∑ k, i.symm (j (e k)) • .X k

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ (fun x ↦ (algebraMap K L) (a x)) = fun x ↦ 0

Tactic:
rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ (fun x ↦ (algebraMap K L) (a x)) = fun x ↦ 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
x✝ : x ∈ nilradical R
n : ℕ
h : x ^ n ∈ 0
⊢ x ^ p ^ n = 0

Tactic:
← Nat.sub_add_cancel ((n.lt_pow_self hp).le),

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
x✝ : x ∈ nilradical R
n : ℕ
h : x ^ n ∈ 0
⊢ x ^ (p ^ n - n + n) = 0
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
⊢ a * 0 = 0

Tactic:
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
      rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
      simp only [iterate_zero, id_eq, iterate_map_zero, mul_zero, mk_zero_right]

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
⊢ ↑(((proj { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }) g) x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
let : IsScalarTower k L L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((proj { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }) g) x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
r : R
hr : x = r ^ n
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
exact ⟨r⁻¹, by simpa using hr⟩

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
exact ⟨r⁻¹, by simpa using hr⟩

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

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

Tactic:
obtain ⟨m, hm⟩ := exists_pow_mem_center_of_inseparable' p ha hinsep
  refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩
  have inter : (ad k D a)^[p ^ m] = 0 := by
    ext x
    rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), LinearMap.sub_apply,
      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
      Subring.mem_center_iff.1 hm.2 x]
    exact sub_eq_zero_of_eq rfl
  rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ⋃ i ∈ ∅, g i • ↑(H i) = Set.univ
⊢ False

Tactic:
rw [← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ∅ = Set.univ
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case inr
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
⊢ (nthRoots n a).card = (X ^ n - C a).natDegree

Tactic:
hζ.card_nthRoots,

Goal state after:
case inr
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
⊢ (if ∃ α, α ^ n = a then n else 0) = (X ^ n - C a).natDegree
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥B
i : ι
⊢ (H.basisOfBasisRight H' b) i = (algebraMap (↥B) S) (b i)

Tactic:
simp [basisOfBasisRight]

Goal state after:
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 B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
nontriviality R

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

Tactic:
have := hfa.isDomain fa.toRingHom

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
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
⊢ False
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ (trace F F) a = a

Tactic:
trace_self_apply

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ a = a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ minpoly K a = X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a)

Tactic:
by
  classical
  exact Classical.choose_spec <| Nat.find_spec <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

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
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B

Tactic:
nontriviality R

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

Tactic:
nontriviality R

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 * finrank 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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ ∀
    x ∈
      (have this := ⋯;
        Subalgebra.perfectClosure F E (ringExpChar F)).carrier,
    x⁻¹ ∈
      (have this := ⋯;
        Subalgebra.perfectClosure F E (ringExpChar F)).carrier

Tactic:
rintro x ⟨n, hx⟩
    use n; rw [inv_pow]
    apply inv_mem (id hx : _ ∈ (⊥ : IntermediateField F E))

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✝¹ : 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:
nontriviality R

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✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime (finrank 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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) =
    Subalgebra.toSubmodule (Algebra.adjoin F ((fun x ↦ x ^ q ^ n) '' Set.univ))

Tactic:
Set.image_univ,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) =
    Subalgebra.toSubmodule (Algebra.adjoin F (Set.range fun x ↦ x ^ q ^ n))
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ Irreducible (f.minpolyX ↥K⟮f⟯)

Tactic:
rw [← f.minpolyX_map K[f] K⟮f⟯,
    ← IsPrimitive.irreducible_iff_irreducible_map_fraction_map]

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ Irreducible (f.minpolyX ↥K[f])

K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : UniqueFactorizationMonoid ↥K[f]
⊢ (f.minpolyX ↥K[f]).IsPrimitive
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
simp_all [RatFunc.intDegree_mul]

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)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1

Tactic:
s.independent.finrank_vectorSpan (Fintype.card_fin _),

Goal state after:
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)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ n = finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case h
𝕜 : 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₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ inner 𝕜 (p₁ -ᵥ ↑((orthogonalProjection s) p₂)) (↑((orthogonalProjection s) p₂) -ᵥ p₂) = 0

Tactic:
exact Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
    (orthogonalProjection_vsub_mem_direction_orthogonal s p₂)

Goal state after: