mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l

Goal state after:
case h1
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝² : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
x✝¹ : LiftRelO R (LiftRel R) none none
x✝ : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
by
          have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Finsupp

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
f : α →₀ M₀
⊢ ↑f.support.sym2 = map ⇑f ⁻¹' Function.support mul

Tactic:
ext ⟨a, b⟩; simp

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f

Tactic:
by
    simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
    ext x
    cases x

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
n✝ : ℕ
p : α → Prop
v✝ : Vector3 α n✝
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)
⊢ p a

Tactic:
simpa using h fz

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ aestabilizer G μ s

Tactic:
cases eventuallyConst_set'.mp hs with
  | inl h => simp [aestabilizer_congr h]
  | inr h => simp [aestabilizer_congr h]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ (f.comp g.toOrderHom).toFun (x + 1) = (f.comp g.toOrderHom).toFun x + 1

Tactic:
simp [map_add_one]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 / ↑n ≤ (g ^ n) 0 / ↑n

Tactic:
gcongr; exact pow_mono h _ _

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
⊢ z < τ f

Tactic:
by
  obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
  refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_
  apply le_translationNumber_of_add_le
  simp only [← le_sub_iff_add_le']
  exact f.forall_map_sub_of_Icc _ hx

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
n : ℕ
⊢ Continuous ⇑(f ^ n)

Tactic:
by
  rw [coe_pow]
  exact hf.iterate n

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

Goal state before:
pp: 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)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)

Tactic:
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]

Goal state after:
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)))
δ : ι → ℝ := fun j ↦ T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[>] 0)
⊢ Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
Module: Mathlib.Dynamics.Ergodic.AddCircleAdd

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
⊢ Ergodic (fun x ↦ x + a) volume ↔ addOrderOf a = 0

Tactic:
simp only [add_comm, ← ergodic_add_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in Filter.map (fun a ↦ a + k) atTop, f^[n] x ∈ s

Tactic:
frequently_map

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddGroup τ
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s = s
t : τ
⊢ ϕ.toFun t '' s ⊆ s

Tactic:
h t

Goal state after:
τ : Type u_1
α : Type u_2
inst✝² : TopologicalSpace τ
inst✝¹ : TopologicalSpace α
inst✝ : AddGroup τ
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s = s
t : τ
⊢ s ⊆ s
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 : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
← s_card

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ ↑s.card < ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
← s_card

Goal state after:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card
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 ∂ν = (ν.withDensity (μ.rnDeriv ν)) s ∨
    ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0

Tactic:
← withDensity_apply _ hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
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
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
← s_card

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
⊢ coverMincard T F (U ○ U) n ≤ ↑s.card
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
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy S F ≤ coverEntropy S F

Tactic:
exact coverEntropy_antitone S F (uniformContinuous_iff_le_comap.1 h')

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ μ.real t = μ.real s

Tactic:
by rw [measureReal_def, measureReal_def, measure_toMeasurable s]

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

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

Tactic:
by
  rw [← expGrowthSup_const one_ne_zero one_ne_top, netEntropyEntourage]
  simp only [netMaxcard_univ T h, ENat.toENNReal_one]

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F G : Set X
F_G : F ⊆ G
n : ℕ
⊢ ↑(netMaxcard T F U n) ≤ ↑(netMaxcard T G U n)

Tactic:
exact ENat.toENNReal_mono (netMaxcard_monotone_subset T U n F_G)

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

Goal state before:
pp: R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ = Cardinal.lift.{max u v, w} #ι

Tactic:
rw [max_eq_left, max_eq_right]

Goal state after:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι

R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)
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 (funMap f' x) = funMap f' (⇑f.symm ∘ x)

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
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
⊢ funMap f' x = f.toEquiv (funMap f' (⇑f.symm ∘ x))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
a✝ : α
f : ↥(var a✝).varFinset → β
hv' : ∀ (a : ↥(var a✝).varFinset), v (f a) = v' ↑a
⊢ realize v ((var a✝).restrictVar f) = realize v' (var a✝)

Tactic:
simp [restrictVar, hv']

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃' θ).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
by
  rw [BoundedFormula.ex, realize_not, realize_all, not_forall]
  simp_rw [realize_not, Classical.not_not]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
⊢ (∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)

Tactic:
simp only [← Fin.comp_snoc]

Goal state after:
case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
⊢ (∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Quotient.mk' ∘ Fin.snoc v m)) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
rw [mk_sigma]
    refine (sum_le_lift_mk_mul_iSup _).trans ?_
    rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
      ciSup_le_iff' bddAbove_of_small]
    · refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩
      refine max_le (le_max_left _ _) ?_
      grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
    · rw [← Cardinal.one_le_iff_ne_zero]
      refine _root_.trans ?_ (le_ciSup bddAbove_of_small 1)
      rw [Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]
      exact ⟨var (Sum.inr 0)⟩

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: 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
h : ∅ ∈ (closure L).closed
⊢ x ∉ ⊥

Tactic:
rw [← closure_empty, ← SetLike.mem_coe, h]

Goal state after:
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
h : ∅ ∈ (closure L).closed
⊢ x ∉ ∅
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ ↑((closure L).toFun A) = A

Tactic:
refine Subset.antisymm ?_ subset_closure
  rw [coe_closure_eq_range_term_realize]
  intro x hx
  have : A.Definable₁ L {x} := by
    obtain ⟨t, rfl⟩ := hx
    use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants
    simp [Set.ext_iff]
  exact singleton_inter_nonempty.mp <| hA _ (singleton_nonempty x) this

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝³ : L.Structure M
α : Type u'
inst✝² : DecidableEq α
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
h : M ⊨ equivSentence φ
⊢ Realize (BoundedFormula.restrictFreeVar φ id) fun a ↦ ↑(L.con ↑a)

Tactic:
simpa [Formula.Realize, BoundedFormula.realize_restrictFreeVar] using h

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
a : M
⊢ {a}.Definable₁ L {a}

Tactic:
exists (Term.var 0).equal (L.con (⟨a, rfl⟩ : ↑({a} : Set M))).term

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ (algebraMap k (MvPolynomial σ k ⧸ I)).IsIntegral

Tactic:
exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective

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

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc✝ : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ ↑s * ↑s' = ↑s' * ↑s

Tactic:
· exact_mod_cast hc

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i ↦ (eval v) (↑p i);
      let S := {x | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

Tactic:
have injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → (ι → K)),
      S.InjOn f ↔ ∀ x y, x ∈ S → y ∈ S → f x = f y → x = y := by
    simp [Set.InjOn]; tauto

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
injOnAlt : ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
⊢ K ⊨ genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      let f := fun v i ↦ (eval v) (↑p i);
      let S := {x | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖

Tactic:
refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ IsPrimePow ‖α‖ → Nonempty (Field α)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)).subtype.range = ⊤

Tactic:
range_subtype

Goal state after:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E

Tactic:
rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]

Goal state after: