harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
private lemma id_map : (id : VariableChange R).map φ = id

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 } = { u := 1, r := 0, s := 0, t := 0 }

Tactic:
ext <;> simp only [map_one, Units.val_one, map_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ map φ id = id

Tactic:
simp only [id, map]

Result:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 } = { u := 1, r := 0, s := 0, t := 0 }
-- Mathlib/RingTheory/Smooth/Basic.lean
theorem of_isLocalization : FormallySmooth R Rₘ

Proof state:
case comp_surjective
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
have : ∀ x : M, IsUnit (algebraMap R Q x) := by
  intro x
  apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
  convert (IsLocalization.map_units Rₘ x).map f
  simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]

Result:
case comp_surjective
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ IsUnit ((Ideal.Quotient.mk I) ((algebraMap R Q) ↑x))

Tactic:
convert (IsLocalization.map_units Rₘ x).map f

Result:
case h.e'_3
R Rₘ : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : ↥M
⊢ (Ideal.Quotient.mk I) ((algebraMap R Q) ↑x) = f ((algebraMap R Rₘ) ↑x)
-- Mathlib/SetTheory/Nimber/Field.lean
theorem exists_of_lt_mul (h : c < a * b) : ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

Proof state:
a b c : Nimber
h : c < a * b
⊢ ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

Tactic:
rw [mul_def] at h

Result:
a b c : Nimber
h : c < sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

Proof state:
a b c : Nimber
h : c < sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
this : c ∉ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

Tactic:
rwa [Set.not_mem_compl_iff] at this

Result:
no goals

Proof state:
a b c : Nimber
h : c < sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c

Tactic:
have := not_mem_of_lt_csInf' h

Result:
a b c : Nimber
h : c < sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
this : c ∉ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictMono_of_pred_lt (hf : ∀ a, ¬ IsMin a → f (pred a) < f a) : StrictMono f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) < f a

Tactic:
simpa using hf

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f

Tactic:
simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_image_le_iff {d : ℝ≥0∞} {f : β → α} {s : Set β} :
    diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Proof state:
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Tactic:
simp only [diam_le_iff, forall_mem_image]

Result:
no goals
-- Mathlib/Topology/Algebra/Indicator.lean
@[to_additive]
protected lemma Continuous.mulIndicator (hs : ∀ a ∈ frontier s, f a = 1) (hf : Continuous f) :
    Continuous (mulIndicator s f)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous f
⊢ Continuous (s.mulIndicator f)

Tactic:
exact hf.piecewise hs continuous_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous f
⊢ Continuous (s.mulIndicator f)

Tactic:
classical exact hf.piecewise hs continuous_const

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Polynomial.lean
@[simp]
lemma KaehlerDifferential.mvPolynomialBasis_repr_D_X (σ) (i) :
    (mvPolynomialBasis R σ).repr (D _ _ (.X i)) = Finsupp.single i 1

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
⊢ (mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1

Tactic:
simp [mvPolynomialBasis_repr_D]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_and_left {p : α → Prop} :
    ∀ l u, Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ a ∈ l, p a) ∧ Forall₂ R l u
  | [], u => by
    simp only [forall₂_nil_left_iff, forall_prop_of_false (not_mem_nil _), imp_true_iff, true_and]
  | a :: l, u => by
    simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      @and_comm _ (p a), @and_left_comm _ (p a), exists_and_left]
    simp only [and_comm, and_assoc, and_left_comm, ← exists_and_right]

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) [] u ↔ (∀ (a : α), a ∈ [] → p a) ∧ Forall₂ R [] u

Tactic:
simp only [forall₂_nil_left_iff, forall_prop_of_false (not_mem_nil _), imp_true_iff, true_and]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x

Tactic:
simp only [and_comm, and_assoc, and_left_comm, ← exists_and_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u

Tactic:
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
  @and_comm _ (p a), @and_left_comm _ (p a), exists_and_left]

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_mul (m : ℕ) : ∀ n : ℕ, ((m * n : ℕ) : Ordinal) = m * n
  | 0 => by simp
  | n + 1 => by rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]

Proof state:
m n : ℕ
⊢ ↑(m * (n + 1)) = ↑m * ↑(n + 1)

Tactic:
rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]

Result:
no goals

Proof state:
m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem isEqv_toArray [BEq α] (a b : Vector α n) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r)

Proof state:
α : Type u_1
n : Nat
r : α → α → Bool
inst✝ : BEq α
a b : Vector α n
⊢ a.isEqv b.toArray r = a.isEqv b r

Tactic:
simp [isEqv_eq_decide, Array.isEqv_eq_decide]

Result:
no goals
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem finite_rat_abs_sub_lt_one_div_den_sq (ξ : ℚ) :
    {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}.Finite

Proof state:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
simp_rw [mem_iUnion]

Result:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ ∃ i, ∃ (_ : i ∈ Ioc 0 ξ.den), xy ∈ Icc (⌈ξ * ↑i⌉ - 1) (⌊ξ * ↑i⌋ + 1) ×ˢ {i}

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
intro xy hxy

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : xy ∈ f '' s
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
-- Mathlib/Data/List/Pairwise.lean
theorem pairwise_of_reflexive_of_forall_ne (hr : Reflexive R)
    (h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → R a b) : l.Pairwise R

Proof state:
case a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
exact heq

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b

Tactic:
cases heq

Result:
case refl
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ ∀ {a b : α}, [a, b] <+ l → R a b

Tactic:
intro a b hab

Result:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b

Proof state:
case a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
(apply hab.subset; simp)

Result:
no goals

Proof state:
case a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

Tactic:
apply hab.subset

Result:
case a.a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ Pairwise R l

Tactic:
rw [pairwise_iff_forall_sublist]

Result:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
⊢ ∀ {a b : α}, [a, b] <+ l → R a b

Proof state:
case a.a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ R a b

Tactic:
apply h <;> try (apply hab.subset; simp)

Result:
case a
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b

Tactic:
if heq : a = b then
  cases heq; apply hr
else
  apply h <;> try (apply hab.subset; simp)
  exact heq

Result:
no goals

Proof state:
case refl
α : Type u_1
R : α → α → Prop
l : List α
hr : Reflexive R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a

Tactic:
apply hr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ 0 < { toList := toList✝ }.size

Tactic:
simp only [mem_toArray] at h

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ toList✝
⊢ 0 < { toList := toList✝ }.size

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ toList✝
⊢ 0 < { toList := toList✝ }.size

Tactic:
simpa using List.length_pos_of_mem h

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
⊢ 0 < l.size

Tactic:
cases l

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ 0 < { toList := toList✝ }.size
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_pos_add_filter_neg [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i) (p : ι → Prop)
    [DecidablePred p] : (f.filter p + f.filter fun i => ¬p i) = f :=
  ext fun i => by
    simp only [add_apply, filter_apply]; split_ifs <;> simp only [add_zero, zero_add]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ((if p i then f i else 0) + if ¬p i then f i else 0) = f i

Tactic:
split_ifs <;> simp only [add_zero, zero_add]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ (filter p f + filter (fun i => ¬p i) f) i = f i

Tactic:
simp only [add_apply, filter_apply]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ((if p i then f i else 0) + if ¬p i then f i else 0) = f i
-- Mathlib/Tactic/NormNum/GCD.lean
theorem int_gcd_helper' {d : ℕ} {x y : ℤ} (a b : ℤ) (h₁ : (d : ℤ) ∣ x) (h₂ : (d : ℤ) ∣ y)
    (h₃ : x * a + y * b = d) : Int.gcd x y = d

Proof state:
case h₂
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ y * b

Tactic:
exact Int.gcd_dvd_right.mul_right _

Result:
no goals

Proof state:
case h₁
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a

Tactic:
exact Int.gcd_dvd_left.mul_right _

Result:
no goals

Proof state:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ x.gcd y ∣ d

Tactic:
rw [← Int.natCast_dvd_natCast, ← h₃]

Result:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b

Proof state:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ x.gcd y = d

Tactic:
refine Nat.dvd_antisymm ?_ (Int.natCast_dvd_natCast.1 (Int.dvd_gcd h₁ h₂))

Result:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ x.gcd y ∣ d

Proof state:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b

Tactic:
apply dvd_add

Result:
case h₁
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a

case h₂
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ y * b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
    (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r))

Tactic:
rw [rotateLeftAux, getLsbD_or]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ ((x <<< r).getLsbD i || (x >>> (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
this : (x >>> (w - r)).getLsbD i = false
⊢ decide (i < r) = false

Tactic:
simp [hi]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
this : (x >>> (w - r)).getLsbD i = false
hiltr : decide (i < r) = false
⊢ ((x <<< r).getLsbD i || (x >>> (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - r))

Tactic:
simp [getLsbD_shiftLeft, Bool.or_false, hi, hiltr, this]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ x.getLsbD (w - r + i) = false

Tactic:
apply getLsbD_ge

Result:
case ge
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ w ≤ w - r + i

Proof state:
case ge
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ w ≤ w - r + i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
this : (x >>> (w - r)).getLsbD i = false
⊢ ((x <<< r).getLsbD i || (x >>> (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - r))

Tactic:
have hiltr : decide (i < r) = false := by
  simp [hi]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
this : (x >>> (w - r)).getLsbD i = false
hiltr : decide (i < r) = false
⊢ ((x <<< r).getLsbD i || (x >>> (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ (x >>> (w - r)).getLsbD i = false

Tactic:
simp only [getLsbD_ushiftRight]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ x.getLsbD (w - r + i) = false

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ ((x <<< r).getLsbD i || (x >>> (w - r)).getLsbD i) = (decide (i < w) && x.getLsbD (i - r))

Tactic:
suffices (x >>> (w - r)).getLsbD i = false by
  have hiltr : decide (i < r) = false := by
    simp [hi]
  simp [getLsbD_shiftLeft, Bool.or_false, hi, hiltr, this]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ (x >>> (w - r)).getLsbD i = false
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_extend_extend (f : α ↪ δ) (g₁ g₂ : α →ᵇ β) (h₁ h₂ : δ →ᵇ β) :
    dist (g₁.extend f h₁) (g₂.extend f h₂) =
      max (dist g₁ g₂) (dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ))

Proof state:
case refine_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

Tactic:
rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)

Result:
case refine_1.inl.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) ((extend f g₂ h₂) (f x)) ≤
    dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)

case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤ dist g₁ g₂ ⊔ dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)]
    {l₁ l₂ : List α} : l₁ ≤ l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁✝ l₂ : List α
h✝ : l₁✝ ++ l₂ < l₁✝
a : α
l₁ : List α
h : a :: l₁ ++ l₂ < a :: l₁
⊢ ?m.118266 ++ ?m.118267 < ?m.118266

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁✝ l₂ : List α
h✝ : l₁✝ ++ l₂ < l₁✝
a : α
l₁ : List α
h : a :: l₁ ++ l₂ < a :: l₁
⊢ False

Tactic:
exact le_append_left (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
⊢ l₁ ≤ l₁ ++ l₂

Tactic:
intro h

Result:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
h : l₁ ++ l₂ < l₁
⊢ False

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
h✝ : l₁ ++ l₂ < l₁
h : [] ++ l₂ < []
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
h : l₁ ++ l₂ < l₁
⊢ False

Tactic:
match l₁, h with
| nil, h => simp at h
| cons a l₁, h => exact le_append_left (by simpa using h)

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_one_iff {x : ℤ√d} : x.norm.natAbs = 1 ↔ IsUnit x :=
  ⟨fun h =>
    isUnit_iff_dvd_one.2 <|
      (le_total 0 (norm x)).casesOn
        (fun hx =>
          ⟨star x, by
            rwa [← Int.natCast_inj, Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _,
              norm_eq_mul_conj, eq_comm] at h⟩)
        fun hx =>
          ⟨-star x, by
            rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h⟩,
    fun h => by
    let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
    have := congr_arg (Int.natAbs ∘ norm) hy
    rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
      Int.natAbs_one, eq_comm, mul_eq_one] at this
    exact this.1⟩

Proof state:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Tactic:
exact this.1

Result:
no goals

Proof state:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : 0 ≤ x.norm
⊢ 1 = x * star x

Tactic:
rwa [← Int.natCast_inj, Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _,
  norm_eq_mul_conj, eq_comm] at h

Result:
no goals

Proof state:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ x.norm.natAbs = 1

Tactic:
rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
  Int.natAbs_one, eq_comm, mul_eq_one] at this

Result:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Proof state:
d : ℤ
x : ℤ√d
h : IsUnit x
⊢ x.norm.natAbs = 1

Tactic:
let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h

Result:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ x.norm.natAbs = 1

Proof state:
d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
⊢ 1 = x * -star x

Tactic:
rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
  Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h

Result:
no goals

Proof state:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
⊢ x.norm.natAbs = 1

Tactic:
have := congr_arg (Int.natAbs ∘ norm) hy

Result:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)
⊢ x.norm.natAbs = 1
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsCycle.rotate {u v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u ∈ c.support) :
    (c.rotate h).IsCycle

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCycle
h : u ∈ c.support
⊢ c.support.tail.Nodup

Tactic:
exact hc.support_nodup

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCycle
h : u ∈ c.support
⊢ (c.rotate h).support.tail.Nodup

Tactic:
rw [List.IsRotated.nodup_iff (support_rotate _ _)]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCycle
h : u ∈ c.support
⊢ c.support.tail.Nodup

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCycle
h : u ∈ c.support
⊢ (c.rotate h).IsCycle

Tactic:
refine ⟨hc.isCircuit.rotate _, ?_⟩

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCycle
h : u ∈ c.support
⊢ (c.rotate h).support.tail.Nodup