mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
apply Cofix.bisim_rel

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : Fix F
⊢ mk x.dest = x

Tactic:
change (Fix.mk ∘ Fix.dest) x = id x

Goal state after:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ (mk ∘ dest) x = id x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
apply Cofix.bisim_rel

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
⊢ ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates

Tactic:
simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h

Goal state after:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
⊢ s.destruct.Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
⊢ ∃ a', some a' ∈ s.head

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o ↦ Option.rec nil Prod.snd o) b)

Tactic:
simp only [comp_apply, liftRel_pure]

Goal state after:
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    exact h.right

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2

Tactic:
exact Sym2.card

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (x ::ᵥ xs).reverse = xs.reverse.snoc x

Tactic:
cases xs
  simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]
  congr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b = f v.head ∨ b ∈ (map f v).tail.toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b

Tactic:
tail_map,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b = f v.head ∨ b ∈ (map f v.tail).toList ↔ f v.head = b ∨ ∃ a, a ∈ v.tail.toList ∧ f a = b
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2.refine_2
α : 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)
i : Fin2 n
⊢ p (v i)

Tactic:
simpa using h (fs i)

Goal state after:
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
⊢ ↑((p - 1).descFactorial n) = (-1) ^ n * ↑n !

Tactic:
descFactorial_eq_prod_range,

Goal state after:
n p : ℕ
h : n ≤ p
⊢ ↑(∏ i ∈ range n, (p - 1 - i)) = (-1) ^ n * ↑n !
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
simpa [has] using (MeasureTheory.quasiMeasurePreserving_mul_right μ a⁻¹).ae ha

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

Goal state after:
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), x + z < f x
x : ℝ
hx : ∀ y ∈ Icc 0 1, f x - x ≤ f y - y
⊢ z < τ f
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
f : C(M × X, X) := { toFun := uncurry fun x1 x2 ↦ x1 • x2, continuous_toFun := ⋯ }
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
exact isClosed_setOfPred_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm
    (measure_ne_top _ _)

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

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ (range fun x ↦ g ^ x) ⊆ ↑(MulAction.aestabilizer G μ s)

Tactic:
← Subgroup.coe_zpowers,

Goal state after:
G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ ↑(Subgroup.zpowers g) ⊆ ↑(MulAction.aestabilizer G μ s)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense
      ↑(AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
          (AddSubgroup.zmultiples ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) a))) ↔
    Dense ↑(AddSubgroup.closure {a, p})

Tactic:
← AddMonoidHom.map_zmultiples,

Goal state after:
a p : ℝ
⊢ Dense
      ↑(AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
          (AddSubgroup.map (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) (AddSubgroup.zmultiples a))) ↔
    Dense ↑(AddSubgroup.closure {a, p})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case h
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ s = AddSubgroup.zmultiples ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) a)

Tactic:
← AddMonoidHom.map_zmultiples,

Goal state after:
case h
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
a : ℝ
ha : AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ s = AddSubgroup.map (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) (AddSubgroup.zmultiples a)
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : 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 : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ False

Tactic:
obtain ⟨N, hN, hmax⟩ : ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0 := by
    rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H
    convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4
    rw [gt_iff_lt, ← not_le, not_imp_comm, mem_ofPred]

Goal state after:
α : 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 : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
⊢ False
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ∃ c, ν = c • μ

Tactic:
by
  have := hfν.rnDeriv_comp_aeEq hμ.toMeasurePreserving
  obtain ⟨c, hc⟩ := hμ.ae_eq_const_of_ae_eq_comp₀ (measurable_rnDeriv _ _).nullMeasurable this
  use c
  ext s hs
  calc
    ν s = ∫⁻ a in s, ν.rnDeriv μ a ∂μ := .symm <| setLIntegral_rnDeriv hνμ _
    _ = ∫⁻ _ in s, c ∂μ := lintegral_congr_ae <| hc.filter_mono <| ae_mono restrict_le_self
    _ = (c • μ) s := by simp

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
⊢ mulShift 1 x = x

Tactic:
by
  ext h; simp [mulShift]

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

Goal state before:
pp: case succ
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni

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

Tactic:
by
  let μ' := ν.withDensity (μ.rnDeriv ν)
  have h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f) :=
    rnDeriv_withDensity_withDensity_rnDeriv_right μ ν hf hf_ne_zero hf_ne_top
  have h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν :=
    (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)).symm
  have hμ' := rnDeriv_withDensity_right_of_absolutelyContinuous
    (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hf hf_ne_zero hf_ne_top
  filter_upwards [h₁, h₂, hμ'] with x hx₁ hx₂ hx_eq
  rw [← hx₁, hx₂, hx_eq]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x

Tactic:
hx3,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ μ.rnDeriv ν x * ν.rnDeriv κ x = 0 x + μ.rnDeriv ν x * ν.rnDeriv κ x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : N
⊢ x✝ = (refl L N) x✝

Tactic:
refl_apply

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : N
⊢ x✝ = x✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ x✝ = (refl L M) x✝

Tactic:
refl_apply

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : M
⊢ x✝ = x✝
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List (L.Term α)
⊢ listDecode (flatMap listEncode l) = l

Tactic:
by
  suffices h : ∀ (t : L.Term α) (l : List (α ⊕ (Σ i, L.Functions i))),
      listDecode (t.listEncode ++ l) = t::listDecode l by
    induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
  intro t l
  induction t generalizing l with
  | var => rw [listEncode, singleton_append, listDecode]
  | @func n f ts ih =>
    rw [listEncode, cons_append, listDecode]
    have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
    simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
    refine ⟨funext (fun i => ?_), ?_⟩
    · simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]
    · simp only [length_map, length_finRange, drop_left']

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
Relations.formula₂,

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

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (∀' f✝).toFormula.Realize v ↔ (∀' f✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rw [toFormula, Formula.Realize, realize_all, realize_all]

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (∀ (a : M),
      (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
        (snoc default a)) ↔
    ∀ (a : M), f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
⊢ listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l

Tactic:
suffices h : ∀ (φ : Σ n, L.BoundedFormula α n)
      (l' : List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))),
      (listDecode (listEncode φ.2 ++ l')) = φ::(listDecode l') by
    induction l with
    | nil =>
      simp [listDecode]
    | cons φ l ih => rw [flatMap_cons, h φ _, ih]
  rintro ⟨n, φ⟩
  induction φ with
  | falsum => intro l; rw [listEncode, singleton_append, listDecode]
  | equal =>
    intro l
    rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
    · simp only [eq_mp_eq_cast, cast_eq, nil_append]
    · simp only
  | @rel φ_n φ_l φ_R ts =>
    intro l
    rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
    have h : ∀ i : Fin φ_l, ((List.map Sum.getLeft? (List.map (fun i : Fin φ_l =>
      Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σ n, L.BoundedFormula α n).fst, ts i⟩ :
        Σ n, L.Term (α ⊕ (Fin n)))) (finRange φ_l) ++ l))[↑i]?).join = some ⟨_, ts i⟩ := by
      intro i
      simp only [Option.join, map_append, map_map, getElem?_fin, id, Option.bind_eq_some_iff,
        getElem?_eq_some_iff, length_append, length_map, length_finRange, exists_eq_right]
      refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
      rw [getElem_append_left, getElem_map]
      · simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]
      · simp only [length_map, length_finRange, is_lt]
    rw [dif_pos]
    swap
    · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
    rw [dif_pos]
    swap
    · intro i
      obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [h2]
    simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq,
      true_and]
    refine ⟨funext fun i => ?_, ?_⟩
    · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [cast_eq_iff_heq]
      exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
    rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]
    rw [length_map, length_finRange]
  | imp _ _ ih1 ih2 =>
    intro l
    simp only at *
    rw [listEncode, List.append_assoc, cons_append, listDecode]
    simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]
  | all _ ih =>
    intro l
    simp only at *
    rw [listEncode, cons_append, listDecode]
    simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]

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₁
s : Set (α → M)
⊢ A.Definable L s ↔ ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

Tactic:
constructor
  · simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_ofPred_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
  · rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ lift.{max u v, max u v} (max ℵ₀ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (max ℵ₀ L.card)

Tactic:
simp only [mk_empty, lift_zero, lift_uzero, zero_add]

Goal state after:
L : Language
⊢ lift.{max u v, max u v} (max ℵ₀ L.card) ≤ lift.{max u v, max u v} (max ℵ₀ L.card)
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
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
refine ⟨Bundled.of N, ⟨?_⟩, hN⟩

Goal state after:
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
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ M ↪ₑ[L] ↑(Bundled.of ↑N)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
· simp only [hφ, not_true, iff_false]
    rw [models_sentence_iff, not_forall]
    refine ⟨h.1.some, ?_⟩
    simp only [Sentence.realize_not, Classical.not_not]
    exact models_sentence_iff.1 hφ _

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: R : Type u
X : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))

Tactic:
by
  rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
    Cardinal.lift_umax.{v, u}, FreeMonoid]

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

Goal state before:
pp: case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
rw [lift_umax.{v, u}, lift_id'] at this

Goal state after:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)