mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) s2.destruct
    t2.destruct

Tactic:
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b
Module: Mathlib.Data.String.Basic

Goal state before:
pp: s₁ s₂ : String
⊢ s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList

Tactic:
rw [String.le_iff_not_lt, lt_iff_toList_lt, not_lt]

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

Goal state before:
pp: case nil.nil.cons
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ s_1 S T_1,
    (s.append T.join).destruct = (s_1.append (S.append T_1).join).destruct ∧
      (s.append T.join).destruct = (s_1.append (S.join.append T_1.join)).destruct

Tactic:
refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) nil = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g nil)

Tactic:
rw [traverse, traverse, map_pure, traverse]

Goal state after:
case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ C a

Tactic:
have : S = T.map (map fun c => c.1) := by
    rw [← WSeq.map_comp]
    refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)
    funext c
    dsimp [id, Function.comp_def]
    rw [← map_comp]
    exact (map_id _).symm

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this : S = WSeq.map (map fun c ↦ c.1) T
⊢ C a
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
by
    refine aeconst_of_dense_setOfPred_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_
    refine (MulAction.dense_orbit M 1).mono ?_
    rintro _ ⟨g, rfl⟩
    simpa using hs g

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
⊢ PreErgodic (⇑f) μ

Tactic:
refine ⟨fun s hsm hs ↦
    aeconst_of_dense_setOfPred_preimage_smul_eq (M := G) hsm.nullMeasurableSet ?_⟩
  refine hf.mono <| iUnion_subset fun n x hx ↦ ?_
  have hsn : f^[n] ⁻¹' s = s := by
    rw [preimage_iterate_eq, iterate_fixed hs]
  rw [mem_preimage, Set.mem_one] at hx
  rw [mem_ofPred, ← hsn]
  ext y
  simp [hx]

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

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ ‖g‖

Tactic:
div_mul_eq_div_div,

Goal state after:
case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / 2 / ↑n + T / 2 / ↑n ≤ ‖g‖
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ f x * μ.rnDeriv ν x) ν

Tactic:
exact hf.mul (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
inst✝² : TopologicalSpace τ
inst✝¹ : AddCommGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x ↦ t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen[inst✝] o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst✝] (image2 ϕ.toFun u s) ∩ o).Nonempty
ϕra : α
ho : ϕra ∈ o
w✝¹ : τ
hr : w✝¹ ∈ u
w✝ : α
ha : w✝ ∈ s
hϕra : ϕ.toFun w✝¹ w✝ = ϕra
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩

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

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x

Tactic:
have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ := withDensity_absolutelyContinuous _ _
    rw [← ν.haveLebesgueDecomposition_add μ]
    suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this
    filter_upwards [h] with _ h _ using h

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
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rw [← t_mincard]

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ ↑t.card
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ))⁻¹ a = (ν + μ).rnDeriv μ a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
Pi.inv_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ) a)⁻¹ = (ν + μ).rnDeriv μ a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h₁
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ Group.IsSolvable (Multiset.prod 0).Gal

pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → Group.IsSolvable s_1.prod.Gal → Group.IsSolvable (insert a s_1).prod.Gal

Tactic:
· exact gal_one_isSolvable

Goal state after:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → Group.IsSolvable s_1.prod.Gal → Group.IsSolvable (insert a s_1).prod.Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

Tactic:
rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ hν₁, withDensity_rnDeriv_eq _ _ hν₂]

Goal state after:
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
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)
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
have hp : p.comp (X ^ n) ≠ 0 := by
    intro h
    rcases comp_eq_zero_iff.mp h with h' | h'
    · exact minpoly.ne_zero (isIntegral_of_mem_solvableByRad (pow_mem hx n)) h'
    · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])

Goal state after:
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
⊢ Group.IsSolvable (minpoly F x).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (h : n✝ ≤ n✝), castLE h f₁✝ = f₁✝
ih2 : ∀ (h : n✝ ≤ n✝), castLE h f₂✝ = f₂✝
h : n✝ ≤ n✝
⊢ castLE h (f₁✝.imp f₂✝) = f₁✝.imp f₂✝

Tactic:
simp [ih1, ih2]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
k n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₁✝) = castLE ⋯ f₁✝
ih2 : ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f₂✝) = castLE ⋯ f₂✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (f₁✝.imp f₂✝)) = castLE ⋯ (f₁✝.imp f₂✝)

Tactic:
simp [ih1, ih2]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ

Tactic:
· simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Tactic:
· simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case rel
α : 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
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ (RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)

Tactic:
conv_lhs => enter [2, i]; erw [term_realize_cast]

Goal state after:
case rel
α : 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
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ (RelMap R✝ fun i ↦ Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ

Tactic:
· simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ ((equivSentence.symm φ).Realize fun a ↦ ↑(L.con a)) ↔ M ⊨ φ

Tactic:
simp only [equivSentence, _root_.Equiv.symm_symm, Equiv.coe_trans, Realize,
    BoundedFormula.realize_relabelEquiv, Function.comp]

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔ M ⊨ φ
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✝
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✝

Tactic:
simp [ih1, ih2]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin β))
  rw [Formula.iAlls]
  simp only [Nat.add_zero, realize_alls, realize_relabel, Function.comp_def,
    castAdd_zero, Sum.elim_map, id_eq]
  refine Equiv.forall_congr ?_ ?_
  · exact ⟨fun v => v ∘ e, fun v => v ∘ e.symm,
      fun _ => by simp [Function.comp_def],
      fun _ => by simp [Function.comp_def]⟩
  · intro x
    rw [Formula.Realize, iff_iff_eq]
    congr
    funext i
    exact i.elim0

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)

Tactic:
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin γ))

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iExs γ φ).Realize v ↔ ∃ i, φ.Realize (Sum.elim v i)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i))

pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)

Tactic:
· exact fun t =>
      isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
        ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
          (aleph0_le_lift.2 (aleph0_le_mk M)))

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
by
  rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
  · exact fun t =>
      isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
        ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
          (aleph0_le_lift.2 (aleph0_le_mk M)))
  · apply Monotone.directed_le
    refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
    simp only [Finset.coe_map, Function.Embedding.coe_subtype]
    exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
      Set.monotone_image fun _ _ => Finset.coe_subset.2

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
inst✝ : Finite X
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_
  obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ · • x)
  wlog! hlt : j < i generalizing i j
  · exact this j i hne.symm heq.symm (hne.lt_of_le hlt)
  use s ^ (i - (j + 1)) • x
  rw [oreDiv_eq_iff]
  refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
  · change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
  · simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

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

Goal state before:
pp: case inr
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
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
suffices Injective j by
    have := lift_mk_le_lift_mk_of_injective this
    rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this

Goal state after:
case inr
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
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
⊢ Injective j
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)),

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ AlgebraicClosure (ZMod p) ⊨ genericPolyMapSurjOnOfInjOn φ mons
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ 0 ^ n - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
hg : (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
    (expand p) p✝ + (expand p) q✝

Tactic:
rw [hf, hg]

Goal state after:
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
⊢ indicator c ∈ restrictDegree σ K (Fintype.card K - 1)

Tactic:
classical
  rw [mem_restrictDegree_iff_sup, indicator]
  intro n
  refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
  simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
    map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
  trans
  · refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim
  · rw [Multiset.count_singleton_self, mul_one]

Goal state after: