mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.149} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j ↦ μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
⊢ μ s = ENNReal.ofReal T

Tactic:
replace hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1) := by
    let δ : ι → ℝ := fun j => T / (2 * ↑(n j))
    have hδ₀ : ∀ᶠ j in l, 0 < δ j :=
      (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
    have hδ₁ : Tendsto δ l (𝓝[>] 0) := by
      refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩
      replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
        (tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
      convert! hu₂.inv_tendsto_atTop
      ext j
      simp only [δ, Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]
    have hw : ∀ᶠ j in l, d ∈ closedBall d (1 * δ j) := hδ₀.mono fun j hj => by
      simp only [one_mul, mem_closedBall, dist_self]
      apply hj.le
    exact hd _ δ hδ₁ hw

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
⊢ μ s = ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case e'_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 : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ x✝ < a✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝

Tactic:
← not_le,

Goal state after:
case e'_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 : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ ¬a✝ ≤ x✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case e'_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 : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ ¬a✝ ≤ x✝ → μ (t a✝) = 0 ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝

Tactic:
not_imp_comm,

Goal state after:
case e'_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 : {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0}.Finite
x✝ a✝ : ℕ
⊢ ¬μ (t a✝) = 0 → a✝ ≤ x✝ ↔ a✝ ∈ {n | μ (s ∩ f^[n] ⁻¹' s) ≠ 0} → a✝ ≤ x✝
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))
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
have : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype

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
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ volume s = addOrderOf u • volume (s ∩ I)

Tactic:
have : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype

Goal state after:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
⊢ volume s = addOrderOf u • volume (s ∩ I)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
rw [← hx₁, hx₂, hx_eq]

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n ≠ 0 ↔ F ≠ ∅

Tactic:
exact not_iff_not.2 (netMaxcard_eq_zero_iff T F U n)

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 : ∃ a, ∃ (b : IsDynCoverOf T F U n ↑a), ↑(#↑⟨a, b⟩) = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
simp only [Nat.cast_inj, exists_prop] at key

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 : ∃ a, IsDynCoverOf T F U n ↑a ∧ #a = k
⊢ ∃ 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✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]
    simp

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
⊢ coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U

Tactic:
refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)
  exact coverEntropyEntourage_le_log_coverMincard_div F_inv (Nat.one_le_iff_ne_zero.1 m_pos)

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

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ ↑(coverMincard T (F ∪ G) U n) ≤ ((fun n ↦ ↑(coverMincard T F U n)) + fun n ↦ ↑(coverMincard T G U n)) n

Tactic:
rw [Pi.add_apply, ← ENat.toENNReal_add]

Goal state after:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ ↑(coverMincard T (F ∪ G) U n) ≤ ↑(coverMincard T F U n + coverMincard T G U n)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict s) = μ s

Tactic:
hs_eq,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ ∫⁻ (a : β), (map f μ).rnDeriv (map f ν) a ∂map f (ν.restrict (f ⁻¹' f '' s)) = μ (f ⁻¹' f '' s)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial ι R ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
refine (AlgEquiv.ofAlgHom (MvPolynomial.rename e)
      (MvPolynomial.rename e.symm) ?_ ?_).toRingEquiv.trans ?_

Goal state after:
case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm) = AlgHom.id R (MvPolynomial κ R)

case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e) = AlgHom.id R (MvPolynomial ι R)

case refine_3
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial κ R ≃+* ↥(Algebra.adjoin R (Set.range w))
Module: Mathlib.FieldTheory.AbelRuffini

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

pp: case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

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

Tactic:
· exact splits_X_pow_sub_one_of_X_pow_sub_C _ n hx (SplittingField.splits _)

Goal state after:
case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ solvableByRad F E ≤ algebraicClosure F E

Tactic:
by
  refine solvableByRad_le fun x n hn hx ↦ ?_
  rw [mem_algebraicClosure_iff] at hx ⊢
  obtain ⟨p, h1, h2⟩ := hx
  refine ⟨p.comp (X ^ n), ⟨fun h ↦ h1 (leadingCoeff_eq_zero.mp ?_), ?_⟩⟩
  · rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h
    rwa [natDegree_X_pow]
  · simpa [aeval_comp]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
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)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable
    (C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod.comp (X ^ n)).Gal

Tactic:
apply gal_mul_isSolvable (gal_C_isSolvable _)

Goal state after:
case hq.refine_2
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] := ⋯
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable ((Multiset.map (fun x ↦ X - C x) s).prod.comp (X ^ n)).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)

Tactic:
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
    rcases g x with l | r <;> simp

Goal state after:
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₂✝
⊢ ((LHom.id L).onBoundedFormula f₁✝).imp ((LHom.id L).onBoundedFormula f₂✝) = id (f₁✝.imp f₂✝)

Tactic:
ih1,

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 ((LHom.id L).onBoundedFormula f₂✝) = id (f₁✝.imp f₂✝)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
rw [Cardinal.le_def]
      refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩
      rintro (a | a) (b | b) h
      · simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h
        rw [h]
      · simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h
      · simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h
        rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ (f₁✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs → (f₂✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs ↔
    f₁✝.Realize v' xs → f₂✝.Realize v' xs

Tactic:
ih1,

Goal state after:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ f₁✝.Realize v' xs → (f₂✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs ↔ f₁✝.Realize v' xs → f₂✝.Realize v' xs

case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ∀ (a : ↥f₁✝.freeVarFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
  exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5.refine_1
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) (f a))

Tactic:
exact h (f a)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ f₁✝.toFormula.Realize v → Realize f₂✝.toFormula v default ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
ih1,

Goal state after:
case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr) → Realize f₂✝.toFormula v default ↔
    (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (s ⇨ t)

Tactic:
rw [himp_eq]; exact ht.union hs.compl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h₁
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 : α ≃ β
i : β → M
b : β
⊢ (fun g ↦ g ∘ ⇑f.symm) ((fun g ↦ g ∘ ⇑f) i) b = i b

Tactic:
simp only [Function.comp_apply, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) → f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
ih1,

Goal state after:
case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize v xs → f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ Std.Symm fun x y ↦ RelMap r ![x, y]

Tactic:
rw [symm_def]
  exact forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ realize_rel₂

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

Goal state before:
pp: 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✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ (B.val a)′ = B.val a′

Tactic:
algHom_deriv'

Goal state after:
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✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ (B.val a)′ = (B.val a)′

case hf
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✝² : Differential K
inst✝¹ : DifferentialAlgebra F K
B : IntermediateField F K
inst✝ : FiniteDimensional F ↥B
a : ↥B
⊢ Function.Injective ⇑B.val