mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ x ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}

Tactic:
Set.mem_one

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
⊢ x ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}
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 / (2 * ↑n) + T / (2 * ↑n) ≤ ‖g + x - x‖

Tactic:
add_sub_cancel_right,

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 / (2 * ↑n) + T / (2 * ↑n) ≤ ‖g‖
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x

Tactic:
exact ae_of_all _ (fun x hx ↦ hx.pos)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
| ∫⁻ (a : α) in s, f a ∂μ

Tactic:
← Measure.withDensity_rnDeriv_eq _ _ hμν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
| ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν

Tactic:
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
| μ s

Tactic:
← Measure.withDensity_rnDeriv_eq _ _ hμν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
| (ν.withDensity (μ.rnDeriv ν)) s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ μ s = (0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) s

Tactic:
conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) s
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 h : G
⊢ A

Tactic:
if hmem : h ∈ p.support.image (v * ·) then
    -- package existence of a preimage under (v * ·)
    let ex : ∃ w, w ∈ p.support ∧ v * w = h := by
      simpa [Finset.mem_image] using hmem
    exact p.config (Classical.choose ex)
  else
    exact default

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Tactic:
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
← k_min,

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ↑k ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0

Tactic:
by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne'

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 {x}
⊢ coverMincard T F U 0 ≤ 1

Tactic:
rw [← Finset.coe_singleton] at this

Goal state after:
X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ coverMincard T F U 0 ≤ 1
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ coverMincard T F univ n ≤ 1

Tactic:
rw [← Finset.coe_singleton] at this

Goal state after:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ coverMincard T F univ n ≤ 1
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(netMaxcard T F U n)) ≠ 0

Tactic:
ne_eq,

Goal state after:
case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬(fun n ↦ ↑(netMaxcard T F U n)) = 0
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(coverMincard T F U n)) ≠ 0

Tactic:
ne_eq,

Goal state after:
case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬(fun n ↦ ↑(coverMincard T F U n)) = 0
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬↑(coverMincard T F U 0) = 0 0

Tactic:
coverMincard_zero T h U,

Goal state after:
case h
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬↑1 = 0 0
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst✝ : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
z : X
hz : z ∈ s
hyz : (y, z) ∈ dynEntourage T U n
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n

Tactic:
exact ⟨z, hz, dynEntourage_comp_subset _ _ _ _ ⟨y, hxy, hyz⟩⟩

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

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
inst✝ : UniformSpace X
⊢ coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G)

Tactic:
simp only [coverEntropy, ← iSup_sup_eq]
  exact biSup_congr fun _ _ ↦ coverEntropyEntourage_union

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
⊢ ∀ (a b : (X ^ n - 1).Gal), a * b = b * a

Tactic:
intro σ

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
⊢ ∀ (b : (X ^ n - 1).Gal), σ * b = b * σ
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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
⊢ ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m

Tactic:
intro σ

Goal state after:
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
σ : (X ^ n - 1).Gal
⊢ ∃ m, σ a = a ^ m
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
⊢ ∀ (a_1 b : (X ^ n - C a).Gal), a_1 * b = b * a_1

Tactic:
intro σ

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).Gal), σ * b = b * σ
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), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
intro σ

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
⊢ ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = C (i (X ^ n - C a).leadingCoeff) * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (map i (X ^ n - 1)).Splits

Tactic:
leadingCoeff_X_pow_sub_C hn',

Goal state after:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = C (i 1) * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
relabel,

Goal state after:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ.all = (relabel g φ).all
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case zeroAdd
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K zeroAdd

Tactic:
| zeroAdd =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

pp: case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)

Tactic:
· simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]

Goal state after:
case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
by
  classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    simp only [prodMk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion,
      mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

pp: case func.succ.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Tactic:
· simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]

Goal state after:
case func.succ.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔ φ.Realize x

Tactic:
by
    refine
      _root_.trans ?_
        ((realize_iff_of_model_completeTheory M N
              (((L.lhomWithConstants M).onBoundedFormula φ).subst
                  (Constants.term ∘ Sum.inr ∘ x)).alls).trans
          ?_)
    · simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
    · simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff]
      rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize (relabel g φ) v default ↔ BoundedFormula.Realize φ (v ∘ g) default

Tactic:
relabel,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ (BoundedFormula.relabel (Sum.inl ∘ g) φ).Realize v default ↔ BoundedFormula.Realize φ (v ∘ g) default
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
ha : a ∈ A
⊢ a ∈ ↑((closure L[[↑A]]).toFun s)

Tactic:
simp only [SetLike.mem_coe]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
ha : a ∈ A
⊢ a ∈ (closure L[[↑A]]).toFun s
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : Fin (Classical.choose ⋯) → M
⊢ (fun v ↦ v ∘ ⇑e.symm) ((fun v ↦ v ∘ ⇑e) x✝) = x✝

Tactic:
by simp [Function.comp_def]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : β → M
⊢ (fun v ↦ v ∘ ⇑e) ((fun v ↦ v ∘ ⇑e.symm) x✝) = x✝

Tactic:
by simp [Function.comp_def]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : Fin (Classical.choose ⋯) → M
⊢ (fun v ↦ v ∘ ⇑e.symm) ((fun v ↦ v ∘ ⇑e) x✝) = x✝

Tactic:
by simp [Function.comp_def]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x✝ : γ → M
⊢ (fun v ↦ v ∘ ⇑e) ((fun v ↦ v ∘ ⇑e.symm) x✝) = x✝

Tactic:
by simp [Function.comp_def]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e_v
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
a : (↑A ⊕ α) ⊕ Fin n✝
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) a =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ a

Tactic:
rcases a with (_ | _) | _ <;> rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ↪ β
inst✝ : Finite β
⊢ A.Definable L ((fun g ↦ g ∘ ⇑f) '' s)

Tactic:
classical
    cases nonempty_fintype β
    refine
      (congr rfl (ext fun x => ?_)).mp
        (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
              (Equiv.sumCongr (Equiv.ofInjective f f.injective)
                (Fintype.equivFin (↥(range f)ᶜ)).symm)).image_comp_sumInl_fin
          _)
    simp only [mem_image, exists_exists_and_eq_and]
    refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
    simp

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

Goal state before:
pp: case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ (aeval x) (derivative (minpoly F x)) ≠ 0

Tactic:
ne_eq,

Goal state after:
case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ¬(aeval x) (derivative (minpoly F x)) = 0