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✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
⊢ a ∈ closure[inst✝⁴] (range fun x ↦ g ^ x)

Tactic:
by_contra h

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
⊢ False
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))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
replace hI := hI.trans closedBall_ae_eq_ball.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))
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddZero τ
f₁ : τ → α → α
cont'✝¹ : Continuous (uncurry f₁)
map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'✝ : Continuous (uncurry f₂)
map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'✝ : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ }.toFun t x =
      { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }.toFun t x
⊢ { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ } =
    { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }

Tactic:
by
    congr
    funext
    exact h _ _

Goal state after:
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)
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
have h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν :=
    (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)).symm

Goal state after:
α : 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 ν
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x
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
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ (closure[inst✝] (image2 ϕ (↑i ∩ v) s))ᶜ ⊆ n

Tactic:
sdiff_compl

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k ∩ closure[inst✝] (image2 ϕ (↑i ∩ v) s) ⊆ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
F_nemp : F.Nonempty
x✝ : Nonempty X
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
have s_nemp := h.nonempty F_nemp

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
F_nemp : F.Nonempty
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
exact ⟨t, t_dyncover.of_entourage_subset V_U⟩

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 = coverMincard T F U n
⊢ Nonempty { s // IsDynCoverOf T F U n ↑s }

Tactic:
by_contra h

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 = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
conv_rhs => rw [ν.haveLebesgueDecomposition_add μ, add_comm]
  refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_eq ?_
  exact (rnDeriv_add_right_of_mutuallySingular
    (Measure.mutuallySingular_singularPart ν μ).symm.withDensity).symm

Goal state after:
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
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)

Tactic:
by_contra h

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
⊢ False
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy T (val '' val ⁻¹' F) = coverEntropy T F

Tactic:
image_preimage_coe G F,

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy T (G ∩ F) = coverEntropy T F
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf T (val '' val ⁻¹' F) = coverEntropyInf T F

Tactic:
image_preimage_coe G F,

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf T (G ∩ F) = coverEntropyInf T F
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

Tactic:
rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]
  simp only [coverMincard_univ T h, ENat.toENNReal_one]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' val '' val ⁻¹' F) = coverEntropy T (φ '' F)

Tactic:
image_preimage_coe G F,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' (G ∩ F)) = coverEntropy T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (φ '' val '' val ⁻¹' F) = coverEntropyInf T (φ '' F)

Tactic:
image_preimage_coe G F,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (φ '' (G ∩ F)) = coverEntropyInf T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
rw [coverEntropyInf_eq_iSup_netEntropyInfEntourage T F]
  apply (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩).antisymm'
  refine iSup₂_le fun U U_uni ↦ ?_
  obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
  apply (netEntropyInfEntourage_antitone T F si_U).trans
  exact le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ netEntropyInfEntourage T F (s i)) i h_i

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]

Goal state after:
X : Type u_1
T : X → X
F G : Set X
inst✝ : UniformSpace X
⊢ ⨆ U ∈ 𝓤 X, coverEntropyEntourage T (F ∪ G) U =
    ⨆ x ∈ 𝓤 X, max (coverEntropyEntourage T F x) (coverEntropyEntourage T G x)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
by
  by_cases hn : n = 0
  · rw [hn, pow_zero, sub_self]
    exact gal_zero_isSolvable
  have hn' : 0 < n := pos_iff_ne_zero.mpr hn
  have hn'' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
  apply Group.isSolvable_of_comm
  intro σ τ
  ext a ha
  simp only [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha
  have key : ∀ σ : (X ^ n - 1 : F[X]).Gal, ∃ m : ℕ, σ a = a ^ m := by
    intro σ
    lift n to ℕ+ using hn'
    exact map_rootsOfUnity_eq_pow_self σ.toAlgHom (rootsOfUnity.mkOfPowEq a ha)
  obtain ⟨c, hc⟩ := key σ
  obtain ⟨d, hd⟩ := key τ
  rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G

Tactic:
obtain ⟨Gf, Gr⟩ := G

Goal state after:
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }
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 : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ f.symm.toFun (funMap f' x) = funMap f' (f.symm.toFun ∘ x)

Tactic:
simp only [Equiv.toFun_as_coe]
      rw [Equiv.symm_apply_eq]
      refine Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm
      rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
by
    rw [Function.leftInverse_iff_comp, ← LHom.comp_onTerm, φ.left_inv, LHom.id_onTerm]

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✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t

Tactic:
induction t with
  | var ab => rcases ab with a | b <;> simp [Language.con]
  | func f ts ih =>
    simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
    -- Porting note: below lemma does not work with simp for some reason
    rw [withConstants_funMap_sumInl]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
s : Set M
inst✝ : Countable ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable ↥((closure L).toFun s)

Tactic:
by
  have : Countable s := h.to_subtype
  rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
  exact lift_card_closure_le_card_term.trans mk_le_aleph0

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case equal
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₁✝⟩ :: Sum.inl ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, t₂✝⟩ :: ([] ++ l)) =
    ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l

Tactic:
listDecode,

Goal state after:
case equal
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h : ⟨n✝, equal t₁✝ t₂✝⟩.fst = ⟨n✝, equal t₁✝ t₂✝⟩.fst then ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, equal t₁✝ (⋯.mp t₂✝)⟩
      else default) ::
      listDecode ([] ++ l) =
    ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
n✝ : ℕ
f : L.Functions (n✝ + 1)
⊢ ClosedUnder f ∅

Tactic:
intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
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 : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

Tactic:
intro _ _ _ ih1 ih2 _

Goal state after:
case refine_4
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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula Empty n✝
ih1 : ∀ (xs : Fin n✝ → M), f₁✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁✝.Realize default xs
ih2 : ∀ (xs : Fin n✝ → M), f₂✝.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂✝.Realize default xs
xs✝ : Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).Realize (⇑f ∘ default) (⇑f ∘ xs✝) ↔ (f₁✝ ⟹ f₂✝).Realize default xs✝
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} #L.Symbols)

Tactic:
Symbols,

Goal state after:
L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v} #((l : ℕ) × L.Functions l ⊕ (l : ℕ) × L.Relations l))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure

pp: case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ

Tactic:
· rintro ⟨v, hv⟩
    exact (Formula.realize_exClosure φ).mpr ⟨fun a => v a,
      (BoundedFormula.realize_restrictFreeVar (φ := φ) (f := id) (v := fun a => v a) (v' := v)
        (fun _ => rfl)).2
        (by simpa [Formula.Realize]
          using (realize_equivSentence_symm M (Formula.equivSentence φ) v).2 hv)⟩

Goal state after:
case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Tactic:
rw [← lift_le.{w'}, lift_lift, lift_lift] at h1

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Tactic:
rw [models_iff_not_satisfiable] at h

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Tactic:
rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Tactic:
rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ a = 1

Tactic:
mul_eq_one_iff_of_one_le

Goal state after:
case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

case inr.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

case inr.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

pp: case inr.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

pp: case inr.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t

Tactic:
· exact ht.1

Goal state after:
case inr.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

case inr.hb
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ t
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, (Multiset.countAddMonoidHom n) ((Fintype.card K - 1) • {x}) = Fintype.card K - 1

Tactic:
map_nsmul,

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, (Fintype.card K - 1) • (Multiset.countAddMonoidHom n) {x} = Fintype.card K - 1
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
⊢ (algebraMap S M) s ∈ F.extendRight M

Tactic:
rw [IsScalarTower.algebraMap_apply S F M, IsScalarTower.algebraMap_apply F L M]
  exact ⟨algebraMap F L (algebraMap S F s), by simp, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).1, -(n, x).2) ((n + 1, (frobenius K p) x).1, -(n + 1, (frobenius K p) x).2)

Tactic:
← map_neg

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).1, -(n, x).2) ((n + 1, (frobenius K p) x).1, (frobenius K p) (-x))