awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : ¬x < k
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have hx'₁ : k ≤ x
Tactic: rw [not_lt] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have _1 : k + (x - k) % p ∈ s
Tactic: refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_1 : k + (x - k) % p ∈ s
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have _2 : k ≤ k + (x - k) % p
Tactic: refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_1 : k + (x - k) % p ∈ s
_2 : k ≤ k + (x - k) % p
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have _3 : k + (x - k) % p < k + p
Tactic: refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_1 : k + (x - k) % p ∈ s
_2 : k ≤ k + (x - k) % p
_3 : k + (x - k) % p < k + p
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have _4 : k + (x - k) % p + (x - k) / p * p = x
Tactic: refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s
have hx₁ : k + (x - k) % p + (x - k) / p * p ∈ s
Tactic: rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx
Cleared hypotheses: hx, hx'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : k + (x - k) % p + (x - k) / p * p ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s
have _1 : ∀ (m : ℕ) (hx : k + (x - k) % p + m * p ∈ s), k + (x - k) % p ∈ s
Tactic: generalize (x - k) / p = m at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx' : k ≤ x
m : ℕ
hx : k + (x - k) % p + m * p ∈ s
⊢ k + (x - k) % p ∈ s
have _1 : ∀ (hx : k + (x - k) % p + 0 * p ∈ s), k + (x - k) % p ∈ s
Tactic: induction m with grind
Cleared hypotheses: m, hx
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx' : k ≤ x
m : ℕ
hx : k + (x - k) % p + m * p ∈ s
_1 : ∀ (hx : k + (x - k) % p + 0 * p ∈ s), k + (x - k) % p ∈ s
⊢ k + (x - k) % p ∈ s
have _1₁ : ∀ (n : ℕ),
  (∀ (hx : k + (x - k) % p + n * p ∈ s), k + (x - k) % p ∈ s) →
    ∀ (hx : k + (x - k) % p + (n + 1) * p ∈ s), k + (x - k) % p ∈ s
Tactic: induction m with grind
Cleared hypotheses: m, hx
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p + (x - k) / p * p = x
have _4 : k + ((x - k) % p + (x - k) / p * p) = x
Tactic: rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_4 : k + ((x - k) % p + (x - k) / p * p) = x
⊢ k + (x - k) % p + (x - k) / p * p = x
have _4₁ : k + (x - k) = x
Tactic: rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_4 : k + ((x - k) % p + (x - k) / p * p) = x
_4₁ : k + (x - k) = x
⊢ k + (x - k) % p + (x - k) / p * p = x
have _4₂ : x = x
Tactic: rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
right : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
m : ℕ
⊢ x + m * p ∈ s
have h : x + 0 * p ∈ s
Tactic: induction m with grind
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
right : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
m : ℕ
h : x + 0 * p ∈ s
⊢ x + m * p ∈ s
have h₃ : ∀ (n : ℕ), x + n * p ∈ s → x + (n + 1) * p ∈ s
Tactic: induction m with grind
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
⊢ IsEmpty Language.empty.Symbols
have simp : (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)
Tactic: simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f g : M →[L] N
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : M → N) (map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x))
  (map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x))
  (h : { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun = g.toFun),
  { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
g : M →[L] N
toFun : M → N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
h : { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun = g.toFun
⊢ { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } = g
have mk : ∀ (toFun_1 : M → N)
  (map_fun'_1 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun_1 (funMap f x) = funMap f (toFun_1 ∘ x))
  (map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun_1 ∘ x))
  (h :
    { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun =
      { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M →[L] N }.toFun),
  { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
    { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toFun : M → N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
toFun_1 : M → N
map_fun'_1 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun_1 (funMap f x) = funMap f (toFun_1 ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun_1 ∘ x)
h :
  { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun =
    { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M →[L] N }.toFun
⊢ { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
    { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
have mk : ∀ (map_fun'_2 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x))
  (map_rel'_2 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)),
  { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
    { toFun := toFun, map_fun' := @map_fun'_2, map_rel' := @map_rel'_2 }
Tactic: cases h
Cleared hypotheses: toFun_1, map_fun'_1, map_rel'_1, h
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n : ℕ
x : L.Functions n
x_1 : Fin n → M
⊢ Eq.{u_1 + 1} (α := P)
    (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) (funMap x x_1))
    (funMap x (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x_1))
have simp : Eq.{u_1 + 1} (α := P)
  (funMap x (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x_1)))
  (funMap x (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x_1))
Tactic: simp
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f g : M ↪[L] N
h : Eq (α := (a : M) → N) ((fun (f : M ↪[L] N) ↦ f.toFun) f) ((fun (f : M ↪[L] N) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toEmbedding : M ↪ N)
  (map_fun' :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x))
  (map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x)
  (h :
    Eq (α := (a : M) → N)
      ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
      ((fun (f : M ↪[L] N) ↦ f.toFun) g)),
  { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
g : M ↪[L] N
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) g)
⊢ { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } = g
have mk : ∀ (toEmbedding_1 : M ↪ N)
  (map_fun'_1 :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x))
  (map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x)
  (h :
    Eq (α := (a : M) → N)
      ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
      ((fun (f : M ↪[L] N) ↦ f.toFun)
        { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })),
  { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } =
    { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
⊢ { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' : M ↪[L] N } =
    { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
have mk : toEmbedding = toEmbedding_1
Tactic: congr
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toEmbedding : M ↪ N
map_fun' :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding.toFun (funMap f x) = funMap f (toEmbedding.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding.toFun ∘ x) ↔ RelMap r x
toEmbedding_1 : M ↪ N
map_fun'_1 :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding_1.toFun (funMap f x) = funMap f (toEmbedding_1.toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding_1.toFun ∘ x) ↔ RelMap r x
h :
  Eq (α := (a : M) → N)
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding, map_fun' := @map_fun', map_rel' := @map_rel' })
    ((fun (f : M ↪[L] N) ↦ f.toFun) { toEmbedding := toEmbedding_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 })
⊢ toEmbedding = toEmbedding_1
have mk : ∀ (x : M), Eq.{w' + 1} (α := N) ((toEmbedding : (a : M) → N) x : N) ((toEmbedding_1 : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f f' : M ↪[L] N
h : Eq (α := M →[L] N) ((fun (x : M ↪[L] N) ↦ x.toHom) f) ((fun (x : M ↪[L] N) ↦ x.toHom) f')
⊢ f = f'
have h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective.{w + 1, w' + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ (ofInjective hf).toHom = f
have h : ∀ (x : M), Eq.{w' + 1} (α := N) (((ofInjective hf).toHom : (a : M) → N) x : N) ((f : (a : M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{u_1 + 1} (α := P)
    (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) (funMap f x))
    (funMap f (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x))
have simp : Eq.{u_1 + 1} (α := P)
  (funMap f (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)))
  (funMap f (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x))
Tactic: simp only [Function.comp_apply, map_fun]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw : RelMap.{u, v, u_1} (M := P) r
    (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
  RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
rw :
  RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
    RelMap r x
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw₁ : RelMap.{u, v, w'} (M := N) r ((⇑hmn : (a : M) → N) ∘ x) ↔ RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
rw :
  RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x)) ↔
    RelMap r x
rw₁ : RelMap.{u, v, w'} (M := N) r ((⇑hmn : (a : M) → N) ∘ x) ↔ RelMap r x
⊢ RelMap.{u, v, u_1} (M := P) r
      (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    RelMap r x
have rw₂ : RelMap r x ↔ RelMap r x
Tactic: rw [Function.comp_assoc, map_rel, map_rel]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
hfg : h.comp f = h.comp g
⊢ f = g
have h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
⊢ f = g
have h₁ : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f g : M ≃[L] N
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have mk : ∀ (toEquiv : M ≃ N)
  (map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv.toFun (funMap f x) = funMap f (toEquiv.toFun ∘ x))
  (map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv.toFun ∘ x) ↔ RelMap r x)
  (h₁ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun = g.toFun)
  (h₂ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun = g.invFun),
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } = g
Tactic: cases f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
g : M ≃[L] N
toEquiv : M ≃ N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv.toFun (funMap f x) = funMap f (toEquiv.toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv.toFun ∘ x) ↔ RelMap r x
h₁ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun = g.toFun
h₂ : { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun = g.invFun
⊢ { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } = g
have mk : ∀ (toEquiv_1 : M ≃ N)
  (map_fun'_1 :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv_1.toFun (funMap f x) = funMap f (toEquiv_1.toFun ∘ x))
  (map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv_1.toFun ∘ x) ↔ RelMap r x)
  (h₁ :
    { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.toFun =
      { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.toFun)
  (h₂ :
    { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N }.invFun =
      { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M ≃[L] N }.invFun),
  { toEquiv := toEquiv, map_fun' := @map_fun', map_rel' := @map_rel' : M ≃[L] N } =
    { toEquiv := toEquiv_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
Tactic: cases g
Cleared hypotheses: g, h₁, h₂