harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1

Proof state:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]

Result:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)

Proof state:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)

Tactic:
exact one_ne_zero ∘ And.right

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma sec_spec (s : S) : s * (algebraMap R S) (x ^ (IsLocalization.Away.sec x s).2) =
    algebraMap R S (IsLocalization.Away.sec x s).1

Proof state:
case e_a.h.e_6.h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ x ^ Exists.choose ⋯ = ↑(IsLocalization.sec (Submonoid.powers x) s).2

Tactic:
exact (IsLocalization.sec (Submonoid.powers x) s).2.property.choose_spec

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ s * (algebraMap R S) (x ^ Exists.choose ⋯) = s * (algebraMap R S) ↑(IsLocalization.sec (Submonoid.powers x) s).2

Tactic:
congr

Result:
case e_a.h.e_6.h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ x ^ Exists.choose ⋯ = ↑(IsLocalization.sec (Submonoid.powers x) s).2

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ s * (algebraMap R S) (x ^ (sec x s).2) = (algebraMap R S) (sec x s).1

Tactic:
simp only [IsLocalization.Away.sec, ← IsLocalization.sec_spec]

Result:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ s * (algebraMap R S) (x ^ Exists.choose ⋯) = s * (algebraMap R S) ↑(IsLocalization.sec (Submonoid.powers x) s).2
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bmex_lt_ord_succ_card {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{u}) :
    bmex.{_, u} o f < (succ o.card).ord

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ o.bmex f < (succ o.card).ord

Tactic:
rw [← mk_toType]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ o.bmex f < (succ #o.toType).ord

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ o.bmex f < (succ #o.toType).ord

Tactic:
exact mex_lt_ord_succ_mk (familyOfBFamily o f)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivAt.rpow_const (hf : HasDerivAt f f' x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
    HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x

Proof state:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x

Tactic:
exact hf.rpow_const hx

Result:
no goals

Proof state:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
-- Mathlib/Analysis/Calculus/Deriv/Pi.lean
theorem hasDerivAt_update (x : ι → 𝕜) (i : ι) (y : 𝕜) :
    HasDerivAt (Function.update x i) (Pi.single i (1 : 𝕜)) y

Proof state:
case h.e'_9.h.e
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ Pi.single i = ⇑(ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))

Tactic:
ext z j

Result:
case h.e'_9.h.e.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ Pi.single i z j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Proof state:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : j = i
⊢ z = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : ¬j = i
⊢ 0 j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
simp [Pi.single_eq_of_ne h]

Result:
no goals

Proof state:
case h.e'_9.h.e.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ (if j = i then z else 0 j) = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : j = i
⊢ z = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

case neg
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : ¬j = i
⊢ 0 j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Proof state:
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ HasDerivAt (Function.update x i) (Pi.single i 1) y

Tactic:
convert (hasFDerivAt_update x y).hasDerivAt

Result:
case h.e'_9.h.e
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ Pi.single i = ⇑(ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))

Proof state:
case h.e'_9.h.e.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ Pi.single i z j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
rw [Pi.single, Function.update_apply]

Result:
case h.e'_9.h.e.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ (if j = i then z else 0 j) = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
/-- Helper lemma for `integral_log`: case where `a = 0`. -/
lemma integral_log_from_zero {b : ℝ} : ∫ s in (0)..b, log s = b * log b - b

Proof state:
case inl
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Tactic:
conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]

Result:
case inl
b : ℝ
h : b < 0
⊢ ∫ (t : ℝ) in 0 ..b, log (-t) = b * log b - b

Proof state:
b : ℝ
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Tactic:
rcases lt_trichotomy b 0 with h | h | h

Result:
case inl
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Proof state:
case inl
b : ℝ
h : b < 0
⊢ ∫ (t : ℝ) in 0 ..b, log (-t) = b * log b - b

Tactic:
rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
  integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]

Result:
case inl
b : ℝ
h : b < 0
⊢ -(-b * log b - -b) = b * log b - b

Proof state:
case inl
b : ℝ
h : b < 0
⊢ -(-b * log b - -b) = b * log b - b

Tactic:
ring

Result:
no goals

Proof state:
case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Tactic:
exact integral_log_from_zero_of_pos h

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem add_smul (y z : R[S⁻¹]) (x : X[S⁻¹]) :
    (y + z) • x = y • x + z • x

Proof state:
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)

Tactic:
have ha' : ↑((sb * sa) * s₂) = sb * ra * s₃ := by simp [ha, mul_assoc]

Result:
case c.c.c.mk.mk.intro.mk.mk.intro
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)
-- Mathlib/RingTheory/ZMod.lean
theorem ZMod.ringHom_eq_of_ker_eq {n : ℕ} {R : Type*} [CommRing R] (f g : R →+* ZMod n)
    (h : RingHom.ker f = RingHom.ker g) : f = g

Proof state:
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ f = g

Tactic:
rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
⊢ f = g

Tactic:
have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩

Result:
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = ↑⟨g, ⋯⟩
⊢ f = g

Proof state:
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = ↑⟨g, ⋯⟩
⊢ f = g

Tactic:
rw [Subtype.coe_mk] at this

Result:
n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ f = g
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
lemma apply_smul_sub_smul_sub_eq [CommRing R] [AddCommGroup M] [Module R M]
    (B : LinearMap.BilinForm R M) (x y : M) :
    B ((B x y) • x - (B x x) • y) ((B x y) • x - (B x x) • y) =
      (B x x) * ((B x x) * (B y y) - (B x y) * (B y x))

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
x y : M
⊢ (B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) y * (B y) x) -
      ((B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) x * (B y) y)) =
    (B x) x * ((B x) x * (B y) y) - (B x) x * ((B x) y * (B y) x)

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
x y : M
⊢ (B ((B x) y • x - (B x) x • y)) ((B x) y • x - (B x) x • y) = (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)

Tactic:
simp only [map_sub, map_smul, sub_apply, smul_apply, smul_eq_mul, mul_sub,
  mul_comm (B x y) (B x x), mul_left_comm (B x y) (B x x)]

Result:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
x y : M
⊢ (B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) y * (B y) x) -
      ((B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) x * (B y) y)) =
    (B x) x * ((B x) x * (B y) y) - (B x) x * ((B x) y * (B y) x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem mk_lex_mk [BEq α] (lt : α → α → Bool) {l₁ l₂ : Array α} {n₁ : l₁.size = n} {n₂ : l₂.size = n} :
    (Vector.mk l₁ n₁).lex (Vector.mk l₂ n₂) lt = l₁.lex l₂ lt

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Array α
n₁ : l₁.size = n
n₂ : l₂.size = n
⊢ (match
        (forIn' (List.range' 0 n 1) ⟨none, PUnit.unit⟩ fun a m b =>
            if lt l₁[a] l₂[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (l₁[a] != l₂[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
      | none => false
      | some a => a).run =
    (match
        (forIn' (List.range' 0 n 1) ⟨none, PUnit.unit⟩ fun a m b =>
            if lt l₁[a] l₂[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (l₁[a] != l₂[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
      | none => false
      | some a => a).run

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Array α
n₁ : l₁.size = n
n₂ : l₂.size = n
⊢ { toArray := l₁, size_toArray := n₁ }.lex { toArray := l₂, size_toArray := n₂ } lt = l₁.lex l₂ lt

Tactic:
simp [Vector.lex, Array.lex, n₁, n₂]

Result:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Array α
n₁ : l₁.size = n
n₂ : l₂.size = n
⊢ (match
        (forIn' (List.range' 0 n 1) ⟨none, PUnit.unit⟩ fun a m b =>
            if lt l₁[a] l₂[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (l₁[a] != l₂[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
      | none => false
      | some a => a).run =
    (match
        (forIn' (List.range' 0 n 1) ⟨none, PUnit.unit⟩ fun a m b =>
            if lt l₁[a] l₂[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (l₁[a] != l₂[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
      | none => false
      | some a => a).run
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_conjTranspose [StarRing α] (A : Matrix n n α) : A.adjugateᴴ = adjugate Aᴴ

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate

Tactic:
rw [A.adjugate_transpose, this]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate

Tactic:
have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ

Result:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᴴ = Aᴴ.adjugate

Tactic:
dsimp only [conjTranspose]

Result:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
    ∀ {ifp_n : IntFractPair ℚ},
      IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - n

Proof state:
case zero
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q 0 = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑0

Tactic:
intro ifp_zero stream_zero_eq

Result:
case zero
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑0

Proof state:
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
⊢ IntFractPair.of q = ifp_zero

Tactic:
injection stream_zero_eq

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- `1⁻¹` has exactly the same moves as `1`. -/
lemma inv_one : 1⁻¹ ≡ 1

Proof state:
⊢ 1⁻¹ ≡ 1

Tactic:
rw [inv_eq_of_pos PGame.zero_lt_one]

Result:
⊢ inv' 1 ≡ 1

Proof state:
⊢ inv' 1 ≡ 1

Tactic:
exact inv'_one

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_iff_mul_self_eq_of_pos (h : 0 < y) : √x = y ↔ y * y = x

Proof state:
x y : ℝ
h : 0 < y
⊢ √x = y ↔ y * y = x

Tactic:
simp [sqrt_eq_cases, h.ne', h.le]

Result:
no goals
-- Mathlib/Data/Vector/Zip.lean
theorem zipWith_get (x : Vector α n) (y : Vector β n) (i) :
    (Vector.zipWith f x y).get i = f (x.get i) (y.get i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (List.zipWith f ↑x ↑y).get (Fin.cast ⋯ i) = f ((↑x).get (Fin.cast ⋯ i)) ((↑y).get (Fin.cast ⋯ i))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (zipWith f x y).get i = f (x.get i) (y.get i)

Tactic:
dsimp only [Vector.zipWith, Vector.get]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (List.zipWith f ↑x ↑y).get (Fin.cast ⋯ i) = f ((↑x).get (Fin.cast ⋯ i)) ((↑y).get (Fin.cast ⋯ i))
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma fromRows_row0_isTotallyUnimodular_iff (A : Matrix m n R) :
    (fromRows A (row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ ∃ j s, row m' 0 x✝ = Pi.single j ↑s

Tactic:
refine ⟨default, 0, ?_⟩

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ row m' 0 x✝ = Pi.single default ↑0

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
⊢ ∃ j s, row m' 0 x✝ = Pi.single j ↑s

Tactic:
inhabit n

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ ∃ j s, row m' 0 x✝ = Pi.single j ↑s

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromRows (row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
⊢ ∃ j s, row m' 0 x✝ = Pi.single j ↑s

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ row m' 0 x✝ = Pi.single default ↑0

Tactic:
ext x

Result:
case h
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
x : n
⊢ row m' 0 x✝ x = Pi.single default (↑0) x

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromRows (row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
classical
refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
inhabit n
refine ⟨default, 0, ?_⟩
ext x
simp [Pi.single_apply]

Result:
no goals

Proof state:
case h
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
x : n
⊢ row m' 0 x✝ x = Pi.single default (↑0) x

Tactic:
simp [Pi.single_apply]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem of_subset (a : X) (hfB : B.Finite) :
    IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'

Tactic:
exact hag g hg

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
  intro k hk
  exact Set.biInter_subset_of_mem hk

Result:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_surjective [Nontrivial α] : Function.Surjective (sign : Perm α → ℤˣ) := fun a =>
  (Int.units_eq_one_or a).elim (fun h => ⟨1, by simp [h]⟩) fun h =>
    let ⟨x, y, hxy⟩ := exists_pair_ne α
    ⟨swap x y, by rw [sign_swap hxy, h]⟩

Proof state:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = 1
⊢ sign 1 = a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ sign (swap x y) = a

Tactic:
rw [sign_swap hxy, h]

Result:
no goals