mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.node.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      nil.node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else nil.node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
dsimp only [size_node]; split_ifs
          · simp [node3L, node']; abel
          · simp [node4L, node', sr.2.1.1]; abel

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
⊢ LiftP p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
by
  constructor
  · rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use a, fun i j => (f i j).val
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]; rfl
    intro i j
    apply (f i j).property
  rintro ⟨a, f, h₀, h₁⟩
  use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
  rw [← abs_map, h₀]; rfl

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case mpr
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m

Tactic:
rintro ⟨h₁, h₂⟩
    rcases eq_or_lt_of_le h₁ with (rfl | h₁)
    · exact Or.inl rfl
    · exact Or.inr (le_antisymm h₂ h₁)

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
have t_ih_r := t_ih_r' h_mem
      clear t_ih_l' t_ih_r'
      have t_r_h := Valid'.erase_aux x h.right
      obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
      rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
          (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]
      rw [t_ih_r, h.sz.1]
      have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
      revert h_pos_t_r_size; rcases t_r.size with - | t_r_size <;> intro h_pos_t_r_size
      · cases h_pos_t_r_size
      · simp [Nat.add_assoc]

Goal state after:
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * ↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n

Tactic:
mul_assoc,

Goal state after:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ x = ↑x.num * (↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.inl
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ n, some a ∈ (cons a' s').get? n

Tactic:
exists 0
      simp only [get?, drop, head_cons]
      rw [h]
      apply ret_mem

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by
    rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | ⟨_, b, h⟩)
    · obtain ⟨k, hi, hj⟩ := exists_between h
      obtain ⟨c⟩ : Nonempty (α k) := inferInstance
      exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ _ ha, right _ _ hb⟩

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

Goal state before:
pp: case right.HU
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ swap (LiftRel R) s t ∧ swap (LiftRel (LiftRel R)) S T) →
      ∃ s t S T, s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T

Tactic:
exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

pp: case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
· exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩

Goal state after:
case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
⊢ ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))

Tactic:
refine fun x => ⟨x + 2, ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
⊢ x + 2 ∈ upperBounds (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

Tactic:
have : ∀ x, BddAbove (range fun g => f₂ g⁻¹ (f₁ g x)) := by
    refine fun x => ⟨x + 2, ?_⟩
    rintro _ ⟨g, rfl⟩
    have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
      rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
    calc
      f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) :=
        mono _ (map_lt_add_translationNumber_add_one _ _).le
      _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
      _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := by grw [map_lt_add_translationNumber_add_one]
      _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g ↦ (f₂ g⁻¹) ((f₁ g) x))
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / ↑n ≤ ‖g‖

Tactic:
div_le_iff₀' (by positivity : 0 < (n : ℝ)),

Goal state after:
case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T ≤ ↑n * ‖g‖
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ x ∈ f^[N + m] ⁻¹' s

Tactic:
· simpa only [iterate_add] using! hmt.1.2

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0

Tactic:
intro hm
    rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
    exact this.not_gt hkl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyEntourage T F univ = 0

Tactic:
rw [← expGrowthSup_const one_ne_zero one_ne_top, coverEntropyEntourage]

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthSup fun n ↦ ↑(coverMincard T F univ n)) = expGrowthSup fun x ↦ 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * ((μ + ν).rnDeriv ξ a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹)) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * ((μ + ν).rnDeriv ξ a)⁻¹ * (μ + ν).rnDeriv ξ a) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * ((ν.rnDeriv (μ + ν) a)⁻¹ * (((μ + ν).rnDeriv ξ a)⁻¹ * (μ + ν).rnDeriv ξ a)) =
    μ.rnDeriv (μ + ν) a * (ν.rnDeriv (μ + ν) a)⁻¹
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 ^ (c * d) = (a ^ d) ^ c

Tactic:
pow_mul'

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 ^ d) ^ c = (a ^ d) ^ 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
⊢ σ * τ = τ * σ

Tactic:
ext b hb

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 ∈ (X ^ n - C a).rootSet (X ^ n - C a).SplittingField
⊢ (σ * τ) b = (τ * σ) b
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Goal state after:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Goal state after:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))
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) 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

Tactic:
mul_assoc,

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.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) 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

Tactic:
mul_assoc,

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: 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
f g : M ↪[L] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr
    ext x
    exact funext_iff.1 h x

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
rcases CharP.char_is_prime_or_zero K p with (hp | hp)

Goal state after:
case inl
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)

case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ t :: listDecode (flatMap listEncode l) = t :: l

Tactic:
lih

Goal state after:
case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ t :: l = t :: l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ ts i :: (List.map ts l' ++ listDecode l) = ts i :: List.map ts l' ++ listDecode l

Tactic:
cons_append

Goal state after:
case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ ts i :: (List.map ts l' ++ listDecode l) = ts i :: (List.map ts l' ++ listDecode l)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b

Tactic:
simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h
        rw [h]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), v i ∈ {x | ∃ i, x ∈ S i}
⊢ funMap f v ∈ {x | ∃ i, x ∈ S i}

Tactic:
simp_rw [Set.mem_ofPred] at *

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), ∃ i_1, v i ∈ S i_1
⊢ ∃ i, funMap f v ∈ S i