mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
      (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, sumLexLift_eq_empty, not_and_or, exists_prop, not_forall]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
g : G
⊢ (fun x ↦ g • x) ⁻¹' t =ᵐ[μ] (fun x ↦ g • x) ⁻¹' s

Tactic:
exact tendsto_smul_ae _ _ hst.symm

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| < 1 / |2 ^ (n + 1)|

Tactic:
by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

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

Goal state before:
pp: f : CircleDeg1Lift
⊢ Tendsto (fun n ↦ (f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))

Tactic:
by
  refine
    tendsto_iff_dist_tendsto_zero.2 <|
      squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
        ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))
  dsimp
  have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
  rw [Real.dist_eq, div_sub' (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this,
    Nat.cast_add_one, div_le_div_iff_of_pos_right this, ← Nat.cast_add_one]
  apply dist_pow_map_zero_mul_translationNumber_le

Goal state after:
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 μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
by
  have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := fun s hs =>
    h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).nullMeasurableSet
  refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_
  rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
  exact (hx o hoS hxo).mono fun n hn => hos hn

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic f volume

Tactic:
← he.ergodic_conjugate_iff,

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (⇑e ∘ f ∘ ⇑e.symm) volume
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ IsClosed[Pi.topologicalSpace] (cylinder U x)

Tactic:
by
  simpa [cylinder_eq_set_pi U x] using isClosed_set_pi (by simp)

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst✝¹, inst✝] gb
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')

Tactic:
simp only [omegaLimit_def, mem_iInter, MapsTo]
  intro y hy u hu
  refine map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_mem_image2.2 fun t ht x hx ↦ ?_)
  calc
    ϕ' t (ga x) ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
    _ = gb (ϕ t x) := ht.2 hx |>.symm

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

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

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    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.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ ∃ t, IsDynCoverOf T F U n ↑t ∧ #t ≤ #s ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
use {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}
  simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]
  refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩
  obtain ⟨z, z_s, y_Bz⟩ := h y_F
  exact ⟨z, ⟨z_s, _, (dynEntourage T U n).symm y_Bz, y_F⟩, y_Bz⟩

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h₁
τ : 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
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := ⋯
hk : IsCompact (k \ n)
j : Set τ → Set β := ⋯
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := ⋯
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ ⋂ u ∈ g, u ⊆ u

Tactic:
refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)

Goal state after:
case h₁
τ : 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
hn₂ : ω f ϕ s ⊆ n
v : Set τ
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)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u
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
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ↑k = ⊤

Tactic:
rw [k_min, coverMincard, iInf₂_eq_top]

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 }
⊢ ∀ (i : Finset X), IsDynCoverOf T F U n ↑i → ↑(#i) = ⊤
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
suffices (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
      ∧ ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ by
    refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F

pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)

Tactic:
· refine iSup₂_le fun V V_uni ↦
      (coverEntropyEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyEntourage_image_le h F _).trans ?_
    apply coverEntropyEntourage_le_coverEntropy
    rw [uniformity_comap φ, mem_comap]
    exact ⟨_, symmetrize_mem_uniformity V_uni, .rfl⟩

Goal state after:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := ⋯
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
U : SetRel X X
T : X → X
F : Set X
n : ℕ
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h | h
  · exact h ▸ le_top
  · obtain ⟨t, t_cover, t_mincard⟩ := (coverMincard_finite_iff T F U n).1 h
    rw [← t_mincard]
    exact iSup₂_le fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf t_cover)

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: case refine_1
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun x ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U✝ : Set α
hU : IsOpen U✝
x✝ : U✝.Nonempty
⊢ (⋃ m, (fun x ↦ m • x) ⁻¹' U✝).Nonempty

Tactic:
exact nonempty_iUnion.mpr ⟨1, by simpa only [one_smul]⟩

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (τ a) = τ a ^ c

Tactic:
hd,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ σ (a ^ d) = (a ^ d) ^ c
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (τ b) = τ b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
hd,

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
d : F
hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d
⊢ σ (b * (algebraMap F (X ^ n - C a).SplittingField) d) =
    b * (algebraMap F (X ^ n - C a).SplittingField) d * (algebraMap F (X ^ n - C a).SplittingField) c
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)

Tactic:
intro n g x

Goal state after:
case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
g : L[[↑A]].Functions n
x : Fin n → M
⊢ f.toFun (funMap g x) = funMap g (f.toFun ∘ x)
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
a : FieldAxiom
⊢ toProp K a

Tactic:
cases a with

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
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 ⊕ ℕ)
⊢ ⟨⟨n✝, equal t₁✝ t₂✝⟩.fst, equal t₁✝ (⋯.mp t₂✝)⟩ :: listDecode ([] ++ l) = ⟨n✝, equal t₁✝ t₂✝⟩ :: listDecode l

Tactic:
simp only [eq_mp_eq_cast, cast_eq, nil_append]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (if h :
          ∀ (i : Fin φ_l),
            (List.map Sum.getLeft?
                      (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
              true then
        if h' :
            ∀ (i : Fin φ_l),
              ((List.map Sum.getLeft?
                            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                    ⋯).fst =
                ⟨φ_n, rel φ_R ts⟩.fst then
          ⟨⟨φ_n, rel φ_R ts⟩.fst,
            rel φ_R fun i ↦
              ⋯.mp
                ((List.map Sum.getLeft?
                            (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                    ⋯).snd⟩
        else default
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
rw [dif_pos]

Goal state after:
case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (if h' :
          ∀ (i : Fin φ_l),
            ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).fst =
              ⟨φ_n, rel φ_R ts⟩.fst then
        ⟨⟨φ_n, rel φ_R ts⟩.fst,
          rel φ_R fun i ↦
            ⋯.mp
              ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).snd⟩
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

case rel.hc
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ ∀ (i : Fin φ_l),
    (List.map Sum.getLeft?
              (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.isSome =
      true
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (if h' :
          ∀ (i : Fin φ_l),
            ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).fst =
              ⟨φ_n, rel φ_R ts⟩.fst then
        ⟨⟨φ_n, rel φ_R ts⟩.fst,
          rel φ_R fun i ↦
            ⋯.mp
              ((List.map Sum.getLeft?
                          (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                  ⋯).snd⟩
      else default) ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
rw [dif_pos]

Goal state after:
case rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ ⟨⟨φ_n, rel φ_R ts⟩.fst,
        rel φ_R fun i ↦
          ⋯.mp
            ((List.map Sum.getLeft?
                        (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
                ⋯).snd⟩ ::
      listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

case rel.hc
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join.get
          ⋯).fst =
      ⟨φ_n, rel φ_R ts⟩.fst
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
rw [← hs'] at h1 h2 ⊢

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CompatibleRing K
p : ℕ
inst✝¹ : CharP K p
inst✝ : IsAlgClosed K
⊢ K ⊨ Theory.ACF p

Tactic:
refine Theory.model_union_iff.2 ⟨inferInstance, ?_⟩
  simp only [Theory.model_iff, Set.mem_image,
    forall_exists_index, and_imp]
  rintro _ n hn0 rfl
  simp only [realize_genericMonicPolyHasRoot]
  rintro ⟨p, _, rfl⟩
  exact IsAlgClosed.exists_root p (ne_of_gt
    (natDegree_pos_iff_degree_pos.1 hn0))

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := ⋯
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
intro h T0 hT0
    simpa using h (T0 ∪ {Formula.not φ})
      (by
        simp only [Finset.coe_union, Finset.coe_singleton]
        exact Set.union_subset_union hT0 (Set.Subset.refl _))

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

Goal state before:
pp: case inl
h : IsUnit 0
⊢ 0 = 1

pp: case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1

Tactic:
· exact (not_isUnit_zero h).elim

Goal state after:
case inr
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ Module.rank K (↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1} →₀ K) = #↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1}

Tactic:
by rw [rank_finsupp_self']

Goal state after: