harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_two : s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Result:
case intro
α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ 2 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ s = {x, y}

Tactic:
rw [← h, insert_diff_singleton, insert_eq_of_mem hx]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
refine ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, ?_⟩

Result:
case intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ s = {x, y}

Proof state:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ x ≠ y

Tactic:
rintro rfl

Result:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False

Proof state:
α : Type u_1
s : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ s.encard = 2

Tactic:
rw [hs, encard_pair hne]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ s.encard ≠ 0

Tactic:
rw [h]

Result:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ 2 ≠ 0

Proof state:
case intro
α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_not_mem (fun h ↦ h.2 rfl),
  ← one_add_one_eq_two, WithTop.add_right_inj (WithTop.one_ne_top), encard_eq_one] at h

Result:
case intro
α : Type u_1
s : Set α
x : α
h : ∃ x_1, s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False

Tactic:
exact (h.symm.subset rfl).2 rfl

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩

Result:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
case intro
α : Type u_1
s : Set α
x : α
h : ∃ x_1, s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
obtain ⟨y, h⟩ := h

Result:
case intro.intro
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem det_smul_coords_eq_cramer_coords (x : P) :
    (b.toMatrix b₂).det • b₂.coords x = (b.toMatrix b₂)ᵀ.cramer (b.coords x)

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂)
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
rw [Matrix.isUnit_iff_isUnit_det] at hu

Result:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]

Result:
no goals

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)

Tactic:
have hu := b.isUnit_toMatrix b₂

Result:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂)
⊢ (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsOpen.measure_zero_iff_eq_empty (hU : IsOpen U) :
    μ U = 0 ↔ U = ∅ :=
  ⟨fun h ↦ (hU.measure_eq_zero_iff μ).mp h, fun h ↦ by simp [h]⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen U
h : U = ∅
⊢ μ U = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma toOpens_mono :
    Monotone (toOpens (X := X))

Proof state:
case mk.mk.intro
X : Scheme
V : X.Opens
hV : IsAffineOpen V
f : ↑Γ(X, toOpens ⟨V, hV⟩)
hU : IsAffineOpen (X.basicOpen f)
⊢ toOpens ⟨X.basicOpen f, hU⟩ ≤ toOpens ⟨V, hV⟩

Tactic:
exact X.basicOpen_le _

Result:
no goals

Proof state:
X : Scheme
⊢ Monotone toOpens

Tactic:
rintro ⟨U, hU⟩ ⟨V, hV⟩ ⟨f, rfl⟩

Result:
case mk.mk.intro
X : Scheme
V : X.Opens
hV : IsAffineOpen V
f : ↑Γ(X, toOpens ⟨V, hV⟩)
hU : IsAffineOpen (X.basicOpen f)
⊢ toOpens ⟨X.basicOpen f, hU⟩ ≤ toOpens ⟨V, hV⟩
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma le_collapse_of_insert_mem (ha : a ∉ s) (hf : 0 ≤ f) (hts : t = insert a s) (ht : t ∈ 𝒜) :
    f t ≤ collapse 𝒜 a f s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
rw [collapse_eq ha, ← hts, if_pos ht]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t

Tactic:
split_ifs

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t

Tactic:
exact le_add_of_nonneg_left <| hf _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem two_pow_mod_two_eq_zero {n : Nat} : 2 ^ n % 2 = 0 ↔ 0 < n

Proof state:
n : Nat
⊢ 2 ^ n % 2 = 0 ↔ 0 < n

Tactic:
cases n <;> simp [Nat.pow_succ]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd'_inv_app_f' (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) :
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + { as := b }.as + { as := a }.as = n + { as := ab }.as

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + b + a = n + ab

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ n + b + a = n + ab

Tactic:
rw [← h, add_assoc, add_comm a]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f n = (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem pow_le_pow_right {m n : ℕ} (h : m ≤ n) : I ^ n ≤ I ^ m

Proof state:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

Tactic:
rw [Submodule.pow_zero, one_eq_top]

Result:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ ⊤

Proof state:
case succ.intro
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ npowRec n I * npowRec m.succ I ≤ npowRec (m + 1) I

Tactic:
exact mul_le_left

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m ≤ n
⊢ I ^ n ≤ I ^ m

Tactic:
obtain _ | m := m

Result:
case zero
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : 0 ≤ n
⊢ I ^ n ≤ I ^ 0

case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
h : m + 1 ≤ n
⊢ I ^ n ≤ I ^ (m + 1)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
h : m + 1 ≤ n
⊢ I ^ n ≤ I ^ (m + 1)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h

Result:
case succ.intro
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ (m + 1 + n) ≤ I ^ (m + 1)
-- Mathlib/Algebra/DirectSum/LinearMap.lean
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.

See also `LinearMap.trace_restrict_eq_sum_trace_restrict`. -/
lemma trace_eq_sum_trace_restrict (h : IsInternal N) [Fintype ι]
    {f : M →ₗ[R] M} (hf : ∀ i, MapsTo f (N i) (N i)) :
    trace R M f = ∑ i, trace R (N i) (f.restrict (hf i))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Module.Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i => Module.Free.chooseBasis R ↥(N i)
⊢ (trace R M) f = ∑ i : ι, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
  toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
  ← trace_eq_matrix_trace]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
⊢ (trace R M) f = ∑ i : ι, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
let b : (i : ι) → Basis _ R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Module.Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Module.Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i => Module.Free.chooseBasis R ↥(N i)
⊢ (trace R M) f = ∑ i : ι, (trace R ↥(N i)) (f.restrict ⋯)
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_mul_pow_right {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
    (n m : ℕ) (neq : q ≠ p) : padicValNat q (p^n * q^m) = m

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
neq : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m

Tactic:
exact padicValNat_mul_pow_left m n neq

Result:
no goals

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
neq : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
rw [mul_comm (p^n) (q^m)]

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
neq : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_union_right [DecidableEq β] : image₂ f s (t ∪ t') = image₂ f s t ∪ image₂ f s t' :=
  coe_injective <| by
    push_cast
    exact image2_union_right

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∪ t')) = ↑(image₂ f s t ∪ image₂ f s t')

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∪ ↑t') = image2 f ↑s ↑t ∪ image2 f ↑s ↑t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∪ ↑t') = image2 f ↑s ↑t ∪ image2 f ↑s ↑t'

Tactic:
exact image2_union_right

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) :
    ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Proof state:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Tactic:
refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩

Result:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ b = a + ⟨k, ⋯⟩ + 1

Proof state:
case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h

Result:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Proof state:
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ k < ↑b

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Tactic:
cases n

Result:
case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Proof state:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ b = a + ⟨k, ⋯⟩ + 1

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

Result:
no goals

Proof state:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Tactic:
have hkb : k < b := by omega

Result:
case succ.intro
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

Proof state:
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ⟨k, ⋯⟩ + 1 ≤ b

Tactic:
fin_omega

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem exists_mul_emod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k = gcd n k

Proof state:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k) % ↑k).toNat = ((↑n * n.gcdA k + ↑k * n.gcdB k) % ↑k).toNat
⊢ ∃ m, n * m % k = n.gcd k

Tactic:
rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key

Result:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, n * m % k = n.gcd k

Proof state:
k n : ℕ
hk : n.gcd k < k
⊢ ∃ m, n * m % k = n.gcd k

Tactic:
have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))

Result:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
⊢ ∃ m, n * m % k = n.gcd k

Proof state:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
⊢ ∃ m, n * m % k = n.gcd k

Tactic:
have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)

Result:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (fun m => (m % ↑k).toNat) ↑(n.gcd k) = (fun m => (m % ↑k).toNat) (↑n * n.gcdA k + ↑k * n.gcdB k)
⊢ ∃ m, n * m % k = n.gcd k

Proof state:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ Int.ofNat (n * (n.gcdA k % ↑k).toNat % k) = Int.ofNat (↑n * n.gcdA k % ↑k).toNat

Tactic:
rw [Int.ofNat_eq_coe, Int.natCast_mod, Int.ofNat_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
  Int.ofNat_eq_coe, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod,
  ← Int.mul_emod]

Result:
no goals

Proof state:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, n * m % k = n.gcd k

Tactic:
refine ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj ?_) key.symm⟩

Result:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ Int.ofNat (n * (n.gcdA k % ↑k).toNat % k) = Int.ofNat (↑n * n.gcdA k % ↑k).toNat

Proof state:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (fun m => (m % ↑k).toNat) ↑(n.gcd k) = (fun m => (m % ↑k).toNat) (↑n * n.gcdA k + ↑k * n.gcdB k)
⊢ ∃ m, n * m % k = n.gcd k

Tactic:
simp only at key

Result:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k) % ↑k).toNat = ((↑n * n.gcdA k + ↑k * n.gcdB k) % ↑k).toNat
⊢ ∃ m, n * m % k = n.gcd k
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_mem_ne_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) :
    formPerm l x ≠ x ↔ 2 ≤ l.length

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length

Tactic:
exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x ≠ x ↔ 2 ≤ l.length

Tactic:
rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma level_one (χ : DirichletCharacter R 1) : χ = 1

Proof state:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
a✝ : (ZMod 1)ˣ
⊢ χ ↑a✝ = 1 ↑a✝

Tactic:
simp [units_eq_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
a✝ : (ZMod 1)ˣ
⊢ χ ↑a✝ = 1 ↑a✝
-- Mathlib/Algebra/Lie/Abelian.lean
theorem self_module_ker_eq_center : LieModule.ker R L L = center R L

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
y : L
⊢ y ∈ LieModule.ker R L L ↔ y ∈ center R L

Tactic:
simp only [LieModule.mem_maxTrivSubmodule, LieModule.mem_ker, ← lie_skew _ y, neg_eq_zero]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieModule.ker R L L = center R L

Tactic:
ext y

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
y : L
⊢ y ∈ LieModule.ker R L L ↔ y ∈ center R L
-- Mathlib/CategoryTheory/Shift/Localization.lean
lemma shiftFunctor_comp_inverts (a : A) :
    W.IsInvertedBy (shiftFunctor C a ⋙ L) := fun _ _ f hf =>
  Localization.inverts L W _ (by simpa only [iff] using hf)

Proof state:
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
a : A
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
⊢ W ((shiftFunctor C a).map f)

Tactic:
simpa only [iff] using hf

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma dvd_of_mul_dvd_mul_left (ha : a ≠ 0) (h : a * m ∣ a * n) : m ∣ n

Proof state:
case intro
a m n : ℤ
ha : a ≠ 0
b : ℤ
hb : a * n = a * m * b
⊢ m ∣ n

Tactic:
rw [Int.mul_assoc, Int.mul_eq_mul_left_iff ha] at hb

Result:
case intro
a m n : ℤ
ha : a ≠ 0
b : ℤ
hb : n = m * b
⊢ m ∣ n

Proof state:
a m n : ℤ
ha : a ≠ 0
h : a * m ∣ a * n
⊢ m ∣ n

Tactic:
obtain ⟨b, hb⟩ := h

Result:
case intro
a m n : ℤ
ha : a ≠ 0
b : ℤ
hb : a * n = a * m * b
⊢ m ∣ n

Proof state:
case intro
a m n : ℤ
ha : a ≠ 0
b : ℤ
hb : n = m * b
⊢ m ∣ n

Tactic:
exact ⟨_, hb⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_mkVector_iff {a : α} {n} {l : Vector α n} :
    l = mkVector n a ↔ ∀ (b) (_ : b ∈ l), b = a

Proof state:
α : Type u_1
a : α
n : Nat
l : Vector α n
⊢ l.toArray = (mkVector n a).toArray ↔ ∀ (b : α), b ∈ l → b = a

Tactic:
simpa using Array.eq_mkArray_iff (l := l.toArray) (n := n)

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
l : Vector α n
⊢ l = mkVector n a ↔ ∀ (b : α), b ∈ l → b = a

Tactic:
rw [← toArray_inj]

Result:
α : Type u_1
a : α
n : Nat
l : Vector α n
⊢ l.toArray = (mkVector n a).toArray ↔ ∀ (b : α), b ∈ l → b = a
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_inv (t : TransvectionStruct n R) : t.toMatrix * t.inv.toMatrix = 1

Proof state:
case mk
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix = 1

Tactic:
simp [toMatrix, transvection_mul_transvection_same, t_hij]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.toMatrix * t.inv.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩

Result:
case mk
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix = 1