harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Bits.lean
lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n := calc
  bit a m < 2 * n

Proof state:
m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n

Tactic:
cases b <;> dsimp [bit] <;> omega

Result:
no goals

Proof state:
m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n

Tactic:
cases a <;> dsimp [bit] <;> omega

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem orderOf_sr (i : ZMod n) : orderOf (sr i) = 2

Proof state:
case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1

Tactic:
simp [← r_zero]

Result:
no goals

Proof state:
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1

Tactic:
rw [sq, sr_mul_self]

Result:
no goals

Proof state:
n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2

Tactic:
apply orderOf_eq_prime

Result:
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1

case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma conj_wInner_symm (w : ι → ℝ) (f g : ∀ i, E i) :
    conj ⟪f, g⟫_[𝕜, w] = ⟪g, f⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ (starRingEnd 𝕜) (wInner w f g) = wInner w g f

Tactic:
simp [wInner, map_sum, inner_conj_symm, rclike_simps]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_inv_mul_iff_lt : 1 < b⁻¹ * a ↔ b < a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ 1 < b⁻¹ * a ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_tsub_eq_add_tsub_of_le
    (h : c ≤ b) : a - (b - c) = a + c - b

Proof state:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLE α
h : c ≤ b
⊢ a - (b - c) = a + c - b

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h

Result:
case intro
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - (c + d - c) = a + c - (c + d)

Proof state:
case intro
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - (c + d - c) = a + c - (c + d)

Tactic:
rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
lemma eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0

Proof state:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Tactic:
rw [Int.abs_eq_natAbs] at h2

Result:
m x : ℤ
h1 : m ∣ x
h2 : ↑x.natAbs < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Proof state:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0

Tactic:
by_contra h

Result:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ False

Proof state:
m x : ℤ
h1 : m ∣ x
h2 : ↑x.natAbs < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ False

Tactic:
have := Int.natAbs_le_of_dvd_ne_zero h1 h

Result:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffWithinAt_pi_space :
    ContMDiffWithinAt I 𝓘(𝕜, ∀ i, Fi i) n φ s x ↔
      ∀ i, ContMDiffWithinAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) s x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
s : Set M
x : M
n : WithTop ℕ∞
ι : Type u_16
inst✝² : Fintype ι
Fi : ι → Type u_17
inst✝¹ : (i : ι) → NormedAddCommGroup (Fi i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fi i)
φ : M → (i : ι) → Fi i
⊢ ContMDiffWithinAt I 𝓘(𝕜, (i : ι) → Fi i) n φ s x ↔ ∀ (i : ι), ContMDiffWithinAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) s x

Tactic:
simp only [contMDiffWithinAt_iff, continuousWithinAt_pi, contDiffWithinAt_pi, forall_and,
  writtenInExtChartAt, extChartAt_model_space_eq_id, Function.comp_def, PartialEquiv.refl_coe, id]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Comon_.lean
theorem tensorObj_comul' (A B : Comon_ C) :
    (A ⊗ B).comul =
      (A.comul ⊗ B.comul) ≫ (tensorμ (op A.X) (op B.X) (op A.X) (op B.X)).unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A B : Comon_ C
⊢ (A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ (tensorμ (op A.X) (op B.X) (op A.X) (op B.X)).unop

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Nakayama.lean
theorem exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type*} [CommRing R] {M : Type*}
    [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) :
    ∃ r ∈ I, ∀ n ∈ N, r • n = n

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn✝ : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
n : M
hn : n ∈ N
⊢ -(r - 1) • n = n

Tactic:
simpa [sub_smul] using hr' n hn

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_zero' (x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) 0 x p = cons x p

Proof state:
n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ insertNth 0 x p = cons x p

Tactic:
simp [insertNth_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_mul_right (g : ℝ → F) (a : ℝ) :
    (∫ x : ℝ, g (x * a)) = |a⁻¹| • ∫ y : ℝ, g y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y

Tactic:
simpa only [mul_comm] using integral_comp_mul_left g a

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem Term.realize_mem {α : Type*} (t : L.Term α) (xs : α → M) (h : ∀ a, xs a ∈ S) :
    t.realize xs ∈ S

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
t : L.Term α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S

Tactic:
induction' t with a n f ts ih

Result:
case var
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S

case func
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Proof state:
case var
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S

Tactic:
exact h a

Result:
no goals

Proof state:
case func
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Tactic:
exact Substructure.fun_mem _ _ _ ih

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_add_C_sq (c : R) : derivative ((X + C c) ^ 2) = C 2 * (X + C c)

Proof state:
R : Type u
inst✝ : CommSemiring R
c : R
⊢ derivative ((X + C c) ^ 2) = C 2 * (X + C c)

Tactic:
rw [derivative_sq, derivative_X_add_C, mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem conj_mk (a x : G) : SemiconjBy a x (a * x * a⁻¹)

Proof state:
G : Type u_3
inst✝ : Group G
a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)

Tactic:
unfold SemiconjBy

Result:
G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a

Proof state:
G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_ofReal_im (x : ℝ) : (tan x).im = 0

Proof state:
x : ℝ
⊢ (tan ↑x).im = 0

Tactic:
rw [← ofReal_tan_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem linear_ne_zero (cd : Fin 2 → ℝ) (z : ℍ) (h : cd ≠ 0) : (cd 0 : ℂ) * z + cd 1 ≠ 0

Proof state:
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd 0 = 0

Tactic:
apply_fun Complex.im at h

Result:
cd : Fin 2 → ℝ
z : ℍ
h : (↑(cd 0) * ↑z + ↑(cd 1)).im = Complex.im 0
⊢ cd 0 = 0

Proof state:
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
this : cd 0 = 0
⊢ cd = 0

Tactic:
simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero]
  at h

Result:
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd = 0

Proof state:
case h
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
i : Fin 2
⊢ cd i = 0 i

Tactic:
fin_cases i <;> assumption

Result:
no goals

Proof state:
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd = 0

Tactic:
have : cd 0 = 0 := by
  apply_fun Complex.im at h
  simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false,
    Complex.ofReal_im, Complex.zero_im, Complex.mul_im, mul_eq_zero] using h

Result:
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
this : cd 0 = 0
⊢ cd = 0

Proof state:
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd = 0

Tactic:
ext i

Result:
case h
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
i : Fin 2
⊢ cd i = 0 i

Proof state:
cd : Fin 2 → ℝ
z : ℍ
h : (↑(cd 0) * ↑z + ↑(cd 1)).im = Complex.im 0
⊢ cd 0 = 0

Tactic:
simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false,
  Complex.ofReal_im, Complex.zero_im, Complex.mul_im, mul_eq_zero] using h

Result:
no goals

Proof state:
cd : Fin 2 → ℝ
z : ℍ
h : cd ≠ 0
⊢ ↑(cd 0) * ↑z + ↑(cd 1) ≠ 0

Tactic:
contrapose! h

Result:
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd = 0
-- Mathlib/SetTheory/Cardinal/Subfield.lean
private lemma surjective_ofWType : Function.Surjective (WType.elim _ <| operate s)

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Function.Surjective (WType.elim (↥(closure s)) (Subfield.operate s))

Tactic:
rw [← Set.range_eq_univ]

Result:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Set.range (WType.elim (↥(closure s)) (Subfield.operate s)) = Set.univ

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Set.range (WType.elim (↥(closure s)) (Subfield.operate s)) = Set.univ

Tactic:
exact SetLike.coe_set_eq.mpr (rangeOfWType_eq_top s)

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem quotientInfEquivSupQuotient_symm_apply_left (p p' : Submodule R M) (x : ↥(p ⊔ p'))
    (hx : (x : M) ∈ p) :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨x, hx⟩ :=
  (LinearEquiv.symm_apply_eq _).2 <| by
    rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
hx : ↑x ∈ p
⊢ Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk ⟨↑x, hx⟩)

Tactic:
rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.of_mul_left {f g : R[X]} (h : (f * g).Separable) : f.Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ f.Separable

Tactic:
exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ f.Separable

Tactic:
have := h.of_mul_left_left

Result:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ f.Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ f.Separable

Tactic:
rw [derivative_mul] at this

Result:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ f.Separable
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffOn_Iic (a : ℝ) : UniqueDiffOn ℝ (Iic a) :=
  uniqueDiffOn_convex (convex_Iic a) <| by simp only [interior_Iic, nonempty_Iio]

Proof state:
a : ℝ
⊢ (interior (Iic a)).Nonempty

Tactic:
simp only [interior_Iic, nonempty_Iio]

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_zero : q.lift (0 : ℍ[R,c₁,c₂,c₃]) = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.lift 0 = 0

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_int_add [AddCommGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (n : ℤ) (x : G) : f (↑n + x) = f x + n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem not_of_lt_findIdx {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.findIdx p) :
    p (xs[i]'(Nat.le_trans h (findIdx_le_size p))) = false

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
h : i < findIdx p { toList := xs }
⊢ p { toList := xs }[i] = false

Tactic:
simpa using List.not_of_lt_findIdx (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < findIdx p xs
⊢ p xs[i] = false

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
h : i < findIdx p { toList := xs }
⊢ p { toList := xs }[i] = false

Proof state:
α : Type u_1
p : α → Bool
i : Nat
xs : List α
h : i < findIdx p { toList := xs }
⊢ i < List.findIdx p xs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
    pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h

Proof state:
n : Nat
i : Fin (n + 2)
h : ↑i < n + 1
⊢ (i + 1).pred ⋯ = i.castLT h

Tactic:
rw [Fin.ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]

Result:
n : Nat
i : Fin (n + 2)
h : ↑i < n + 1
⊢ ↑i + 1 < n + 1 + 1

Proof state:
n : Nat
i : Fin (n + 2)
h : ↑i < n + 1
⊢ ↑i + 1 < n + 1 + 1

Tactic:
exact Nat.add_lt_add_right h 1

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isClassified_of_isPrimitiveClassified (hp : h.IsPrimitiveClassified) : h.IsClassified

Proof state:
case h
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = 1 * (m ^ 2 - n ^ 2) ∧ y = 1 * (2 * m * n) ∨ x = 1 * (2 * m * n) ∧ y = 1 * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1

Tactic:
omega

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hp : h.IsPrimitiveClassified
⊢ h.IsClassified

Tactic:
obtain ⟨m, n, H⟩ := hp

Result:
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsClassified

Proof state:
case intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsClassified

Tactic:
use 1, m, n

Result:
case h
x y z : ℤ
h : PythagoreanTriple x y z
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = 1 * (m ^ 2 - n ^ 2) ∧ y = 1 * (2 * m * n) ∨ x = 1 * (2 * m * n) ∧ y = 1 * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_inter_verts_left_eq : G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s

Tactic:
ext <;> simp +contextual [imp_false]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma div_im (z w : ℂ) : (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w

Proof state:
z w : ℂ
⊢ (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w

Tactic:
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_insert_of_not_mem (ha : a ∉ s) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a :=
  pairwise_insert.trans <|
    and_congr_right' <| forall₂_congr fun b hb => by simp [(ne_of_mem_of_not_mem hb ha).symm]

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
ha : a ∉ s
b : α
hb : b ∈ s
⊢ a ≠ b → r a b ∧ r b a ↔ r a b ∧ r b a

Tactic:
simp [(ne_of_mem_of_not_mem hb ha).symm]

Result:
no goals
-- Mathlib/Algebra/Lie/Killing.lean
@[simp] lemma ker_killingForm_eq_bot :
    LinearMap.ker (killingForm R L) = ⊥

Proof state:
R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ LinearMap.ker (killingForm R L) = ⊥

Tactic:
simp [← LieIdeal.coe_killingCompl_top, killingCompl_top_eq_bot]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem WellFoundedLT.finite_ne_bot_of_iSupIndep [WellFoundedLT α]
    {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥}

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem lt_mul_iff_one_lt_left [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) :
    a < b * a ↔ 1 < b :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_right a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
a0 : 0 < a
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_eq_iff_eq_or_add_eq_pi {θ ψ : Angle} : sin θ = sin ψ ↔ θ = ψ ∨ θ + ψ = π

Proof state:
θ ψ : Angle
⊢ θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑π

Tactic:
induction ψ using Real.Angle.induction_on

Result:
case h
θ : Angle
x✝ : ℝ
⊢ θ.sin = (↑x✝).sin ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π

Proof state:
case h
θ : Angle
x✝ : ℝ
⊢ θ.sin = (↑x✝).sin ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π

Tactic:
exact sin_eq_real_sin_iff_eq_or_add_eq_pi

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_formula (φ : L.Formula α) {v : α → M} :
    φ.Realize (g ∘ v) ↔ φ.Realize v

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ φ.Realize (⇑g ∘ v) ↔ φ.Realize v

Tactic:
rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
  Unique.eq_default (g ∘ default)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem basis_toMatrix_mul_linearMap_toMatrix [Finite κ] [Fintype κ'] [DecidableEq ι'] :
    c.toMatrix c' * LinearMap.toMatrix b' c' f = LinearMap.toMatrix b' c f :=
  (Matrix.toLin b' c).injective <| by
    haveI := Classical.decEq κ'
    rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

Proof state:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)

Tactic:
haveI := Classical.decEq κ'

Result:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)

Proof state:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)

Tactic:
rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformEmbedding.of_comp_iff {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} :
    IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformEmbedding g
f : α → β
⊢ IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f

Tactic:
simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]

Result:
no goals