mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u b

Tactic:
rw [← hi]

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
a' : (P F).A
f' : (P F).B a' ⟹ α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
u : Fin2 n
b : α u
i : (P F).B a' u
left✝ : i ∈ univ
hi : f' u i = b
⊢ p u (f' u i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
⊢ Valid' o₁ (insertWith f x (node sz l y r)) o₂ ∧ Raised (node sz l y r).size (insertWith f x (node sz l y r)).size

Tactic:
by
    rw [insertWith, cmpLE]
    split_ifs with h_1 h_2 <;> dsimp only
    · rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
      rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
      refine
        ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩
    · rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_ge h_1 h_2) with ⟨vl, e⟩
      suffices H : _ by
        refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _
      exact Or.inl ⟨_, e, h.3.1⟩
    · have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
      rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
      suffices H : _ by
        refine ⟨h.left.balanceR vr H, ?_⟩
        rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
        exact (e.add_left _).add_right _
      exact Or.inr ⟨_, e, h.3.1⟩

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ih
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a✝ : (P F).A
f'✝ : (P F).drop.B a✝ ⟹ α
f✝ : (P F).last.B a✝ → (P F).W α
⊢ WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a✝ f'✝ f✝) → recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a✝ f'✝ f✝)

Tactic:
case ih a₁ f'₁ f₁ =>
      intro h
      -- Porting note: induction on h doesn't work.
      refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
      · intro a f' f₀ f₁ _h ih; simp only [recF_eq]
        congr 4; funext; apply ih
      · intro a₀ f'₀ f₀ a₁ f'₁ f₁ h; simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]
      · intro x y z _e₁ _e₂ ih₁ ih₂; exact Eq.trans ih₁ ih₂

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ (↑(f i)).1⟩

pp: case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
· rw [← xeq, ← abs_repr u, h, ← abs_map]
      rfl

Goal state after:
case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: ⊢ (if 0 < 0 then 1 else 0) = 0

Tactic:
if_neg (lt_irrefl _)

Goal state after:
⊢ 0 = 0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 = ↑0

Tactic:
Int.cast_zero

Goal state after:
case inr.inl
⊢ 0 = 0
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left✝ : i ∈ univ
hi : f i = u
⊢ p u

Tactic:
rw [← hi]

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
p : α → Prop
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), p (f i)
i : (P F).B a
left✝ : i ∈ univ
hi : f i = u
⊢ p (f i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p u

Tactic:
rw [← hi]

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y

Tactic:
rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩

Goal state after:
case none.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) none none = LiftRelO (Function.swap R) (Function.swap C) none none

case none.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) none (some (hy, jy)) = LiftRelO (Function.swap R) (Function.swap C) none (some (hy, jy))

case some.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) none = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) none

case some.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) (some (hy, jy)) =
    LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) (some (hy, jy))
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
by
    cases h : sel s with
    | none => simp [enumerate_eq_none_of_sel, h]
    | some a' =>
      simp only [enumerate, h]
      exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ s✝

Tactic:
by simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ s✝

Tactic:
by simpa using m

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s

Tactic:
exact mem_of_mem_tail (this h)

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
intro a b ma mb

Goal state after:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.inl
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c'.think

Tactic:
exact think_mem ad

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
by
  apply
    Computation.eq_of_bisim fun c1 c2 =>
      ∃ s,
        c1 = destruct (map f s) ∧
          c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
  · intro c1 c2 h
    obtain ⟨s, h⟩ := h
    rw [h.left, h.right]
    induction s using WSeq.recOn
    case nil | cons => simp
    case think s => exact ⟨s, by simp⟩
  · exact ⟨s, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.cons
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.think
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO Eq fun s1 s2 ↦
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 ↦
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (nil.append (S.think.append SS.join).join).destruct.destruct
    (nil.append (S.think.join.append (map join SS).join)).destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C v

Tactic:
rw [eq_nil v]; apply H

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
⊢ f.transnumAuxSeq 0 = f 0

Tactic:
by simp [transnumAuxSeq]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
⊢ ε / 2 ≠ 0

Tactic:
by simp [hε.ne']

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n

Tactic:
apply s_net.card_le_netMaxcard.trans_lt'

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < ↑s.card
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inl
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
· exact h ▸ le_top

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inl
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
· exact h ▸ le_top

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᵐ[ν] 1
⊢ μ = ν

Tactic:
rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ (σ a)

Tactic:
hc,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ (a ^ c)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ a ^ d = (a ^ d) ^ c

Tactic:
hc,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (a ^ c) ^ d = (a ^ d) ^ c
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
key : (σ b / b) ^ n = 1
c : F
hc : (algebraMap F (X ^ n - C a).SplittingField) c = σ b / b
⊢ σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
hc,

Goal state after:
case h
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
key : (σ b / b) ^ n = 1
c : F
hc : (algebraMap F (X ^ n - C a).SplittingField) c = σ b / b
⊢ σ b = b * (σ b / b)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (τ b) = τ (σ b)

Tactic:
hc,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (τ b) = τ (b * (algebraMap F (X ^ n - C a).SplittingField) c)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ b * (algebraMap F (X ^ n - C a).SplittingField) d =
    b * (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
hc,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ b * (algebraMap F (X ^ n - C a).SplittingField) c * (algebraMap F (X ^ n - C a).SplittingField) d =
    b * (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    (fun f ↦ f.toFun) { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
x : M
⊢ toEmbedding✝¹ x = toEmbedding✝ x

Tactic:
exact funext_iff.1 h x

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - C ((algebraMap F (X ^ n - 1).SplittingField) x)).Gal

Tactic:
apply gal_X_pow_sub_C_isSolvable_aux

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (map (RingHom.id (X ^ n - 1).SplittingField) (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (t.substFunc fun {n} ↦ Functions.term) = t

Tactic:
induction t
  · rfl
  · simp only [substFunc, Functions.term, subst, ‹∀ _, _›]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α k
⊢ relabel g φ.not = (relabel g φ).not

Tactic:
by simp [BoundedFormula.not]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case rad
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
y : E
hn : n ≠ 0
hy : y ^ n ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F (y ^ n)).Gal
⊢ Group.IsSolvable (minpoly F y).Gal

Tactic:
exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
a : FieldAxiom
⊢ K ⊨ a.toSentence

Tactic:
rw [a.realize_toSentence_iff_toProp (K := K)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
a : FieldAxiom
⊢ toProp K a
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
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
t : L.Term α
v : α → M
⊢ Term.realize (⇑g ∘ v) t = g (Term.realize v t)

Tactic:
induction t
  · rfl
  · rw [Term.realize, Term.realize, HomClass.map_fun]
    refine congr rfl ?_
    ext x
    simp [*]

Goal state after: