mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
· obtain ⟨c, hb⟩ := exists_lt b
      exact ⟨⟨j, c⟩, left _ _ h, right _ _ hb⟩

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil
α : 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 α))
⊢ 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 (nil.append SS.join).join).destruct.destruct
    (nil.append (nil.join.append (map join SS).join)).destruct.destruct

Tactic:
simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ a ∈ v.toList ↔ ∃ i, v.get i = a

Tactic:
by
  simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get_toList]
  exact
    ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi, h⟩, fun ⟨i, hi, h⟩ =>
      ⟨i, by rwa [toList_length], h⟩⟩

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 ↦ x • x_1) ⁻¹' s = s

Tactic:
← hsn

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 ↦ x • x_1) ⁻¹' (⇑f)^[n] ⁻¹' s = (⇑f)^[n] ⁻¹' s
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
x✝¹ : Set α
x✝ : MeasurableSet x✝¹
h0 : μ x✝¹ ≠ 0
⊢ ∃ x ∈ x✝¹, ∃ m, m ≠ 0 ∧ id^[m] x ∈ x✝¹

Tactic:
by
      simpa [exists_ne] using! nonempty_of_measure_ne_zero h0

Goal state after:
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))
⊢ Disjoint (g +ᵥ B) B

Tactic:
hBg

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))
⊢ Disjoint (ball (g + x) (T / (2 * ↑n))) B
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (↑n * (T / ↑n))

pp: case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ 2 ≠ 0

Tactic:
mul_div_cancel₀ T (lt_of_lt_of_le zero_lt_one hn).ne.symm

Goal state after:
case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal T

case refine_4
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ 2 ≠ 0
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ s ∈ Iio '' t, s ∈ range Iio

pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y

Tactic:
· exact image_subset_range _ _

Goal state after:
case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
⊢ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
⊢ p.mulShift v (v * w) = p.config w

Tactic:
have hmem : (v * w) ∈ p.support.image (v * ·) :=
    Finset.mem_image.mpr ⟨w, hw, rfl⟩

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : v * w ∈ Finset.image (fun x ↦ v * x) p.support
⊢ p.mulShift v (v * w) = p.config w
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
⊢ p.mulShift v (v * w) = p.config w

Tactic:
have hmem : (v * w) ∈ p.support.image (v * ·) :=
    Finset.mem_image.mpr ⟨w, hw, rfl⟩
  -- existential used in the branch
  have ex : ∃ w', w' ∈ p.support ∧ v * w' = v * w := by
    simpa [Finset.mem_image] using hmem
  -- open the `if` branch as returned by the definition
  have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]
  -- the chosen witness equals w by left-cancellation
  have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2
  have h_eq : Classical.choose ex = w := mul_left_cancel hwv'
  rw [h1, h_eq]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
u : G
hu : u ∈ Finset.image (fun x ↦ g * x) p.support
⊢ x u = p.mulShift g u

Tactic:
rcases Finset.mem_image.mp hu with ⟨w, hw, rfl⟩

Goal state after:
case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
w : G
hw : w ∈ p.support
hu : g * w ∈ Finset.image (fun x ↦ g * x) p.support
⊢ x (g * w) = p.mulShift g (g * w)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v ∈ f, closure[inst✝] (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∃ u ∈ f, closure[inst✝] (image2 ϕ u s) ⊆ n

Tactic:
by
  rcases hc₂ with ⟨v, hv₁, hv₂⟩
  let k := closure (image2 ϕ v s)
  have hk : IsCompact (k \ n) :=
    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
  let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
  have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
  have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u := by
    have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
    rw [this, sdiff_subset_comm, sdiff_iUnion]
    rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
    simp_rw [j, sdiff_compl]
    rw [← inter_iInter]
    exact Subset.trans inter_subset_right hn₂
  rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
  let w := (⋂ u ∈ g, u) ∩ v
  have hw₂ : w ∈ f := by simpa [w, *]
  have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ := by
    apply Subset.trans hg₃
    simp only [j, iUnion_subset_iff, compl_subset_compl]
    intro u hu
    unfold w
    gcongr
    refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
    all_goals exact Subset.rfl
  have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ := by
    simp only [compl_subset_compl]
    exact closure_mono (image2_subset inter_subset_right Subset.rfl)
  have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, sdiff_eq, inter_comm]
  have hw : closure (image2 ϕ w s) ⊆ n :=
    compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
  exact ⟨_, hw₂, hw⟩

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 : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
· obtain ⟨s, _, s_card⟩ := h
    rw [← s_card]
    exact WithTop.coe_lt_top s.card

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ univ
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ univ
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 fun x x_s y y_s ↦ ?_

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
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:
· obtain ⟨t, t_cover, t_mincard⟩ := (coverMincard_finite_iff T F U n).1 h
    rw [← t_mincard]
    exact iSup₂_le fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf t_cover)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  ∀ᵐ (x : α) ∂ν,
    (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x) =
      ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
← Filter.EventuallyEq

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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
⊢ σ ((algebraMap F (X ^ n - C a).SplittingField) a) / (algebraMap F (X ^ n - C a).SplittingField) a = 1

Tactic:
σ.commutes,

Goal state after:
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
⊢ (algebraMap F (X ^ n - C a).SplittingField) a / (algebraMap F (X ^ n - C a).SplittingField) a = 1
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
by
  have := @lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
    (fun x : L =>
      let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
      ⟨p.1, x, by
        dsimp
        have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
        rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]⟩)
    fun x y => by
      intro h
      simp only [Set.coe_ofPred, ne_eq, Set.mem_ofPred_eq, Sigma.mk.inj_iff] at h
      refine (Subtype.heq_iff_coe_eq ?_).1 h.2
      simp only [h.1, forall_true_iff]
  rwa [lift_umax, lift_id'.{v}] at this

Goal state after:
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:
σ.commutes,

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) 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 inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : p = 0
⊢ False

Tactic:
exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
· simp [varsToConstants, constantsToVars, ih]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
· simp [varsToConstants, constantsToVars, ih]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ ∀ φ ∈ Theory.field, K ⊨ φ

Tactic:
simp only [Theory.field, Set.mem_range, exists_imp]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ ∀ (φ : ring.Sentence) (x : FieldAxiom), x.toSentence = φ → K ⊨ φ
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ (id f₁✝).imp ((LHom.id L).onBoundedFormula f₂✝) = id (f₁✝.imp f₂✝)

Tactic:
ih2,

Goal state after:
case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ (id f₁✝).imp (id f₂✝) = id (f₁✝.imp f₂✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula ![t]).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]

Tactic:
realize_rel,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t] i)) ↔ RelMap R ![realize (Sum.elim v xs) t]
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula ![t₁, t₂]).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
realize_rel,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) ↔
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
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 :: listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l

Tactic:
l'ih,

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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (R.formula ![t]).Realize v ↔ RelMap R ![Term.realize v t]

Tactic:
realize_rel,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap R fun i ↦ Term.realize v (![t] i)) ↔ RelMap R ![Term.realize v t]
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (R.formula ![t₁, t₂]).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
realize_rel,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap R fun i ↦ Term.realize v (![t₁, t₂] i)) ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

Tactic:
by
  ext; rfl

Goal state after: