harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem neg_eq : -a = a :=
  calc
    -a = -a + 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a + 0 = -a + -a + a

Tactic:
rw [← neg_add_cancel, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a = -a + 0

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ -a + -a + a = a

Tactic:
rw [add_self, zero_add]

Result:
no goals
-- Mathlib/Data/Fintype/Quotient.lean
@[simp]
lemma finHRecOn_mk {C : (∀ i, Quotient (S i)) → Sort*}
    (a : ∀ i, α i) :
    finHRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (finHRecOn fun x => ⟦a x⟧) = fun f x => f a

Tactic:
ext f h

Result:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ finHRecOn (fun x => ⟦a x⟧) f h = f a

Proof state:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ finHRecOn (fun x => ⟦a x⟧) f h = f a

Tactic:
refine eq_of_heq ((eqRec_heq _ _).trans ?_)

Result:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ HEq (Quotient.hrecOn (finChoice fun x => ⟦a x⟧) f h) (f a)

Proof state:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ HEq (Quotient.hrecOn (finChoice fun x => ⟦a x⟧) f h) (f a)

Tactic:
rw [finChoice_eq]

Result:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ HEq (Quotient.hrecOn ⟦a⟧ f h) (f a)

Proof state:
case h.h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → HEq (f a) (f b)
⊢ HEq (Quotient.hrecOn ⟦a⟧ f h) (f a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : mgf X μ t = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t = 0

Tactic:
simp only [mgf, integral_undef hX]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
lemma exp_strictMono : StrictMono exp

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ ENNReal.ofReal (Real.exp a✝¹) < ENNReal.ofReal (Real.exp a✝)

Tactic:
exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_lt_exp_of_lt (mod_cast h), Real.exp_pos _⟩

Result:
no goals

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

Tactic:
simp_rw [exp_coe]

Result:
case h_real.h_real
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ ENNReal.ofReal (Real.exp a✝¹) < ENNReal.ofReal (Real.exp a✝)

Proof state:
case h_real.h_top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
simp

Result:
no goals

Proof state:
case h_top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Tactic:
exact (not_top_lt h).elim

Result:
no goals

Proof state:
case h_bot
y : EReal
h : ⊥ < y
⊢ ⊥.exp < y.exp

Tactic:
rw [exp_bot, pos_iff_ne_zero, ne_eq, exp_eq_zero_iff]

Result:
case h_bot
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥

Proof state:
case h_bot
y : EReal
h : ⊥ < y
⊢ ¬y = ⊥

Tactic:
exact h.ne'

Result:
no goals

Proof state:
case h_real.h_bot
a✝ : ℝ
h : ↑a✝ < ⊥
⊢ (↑a✝).exp < ⊥.exp

Tactic:
simp at h

Result:
no goals

Proof state:
x y : EReal
h : x < y
⊢ x.exp < y.exp

Tactic:
induction x

Result:
case h_bot
y : EReal
h : ⊥ < y
⊢ ⊥.exp < y.exp

case h_real
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp

case h_top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Proof state:
case h_real
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp

Tactic:
induction y

Result:
case h_real.h_bot
a✝ : ℝ
h : ↑a✝ < ⊥
⊢ (↑a✝).exp < ⊥.exp

case h_real.h_real
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

case h_real.h_top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Proof state:
⊢ StrictMono exp

Tactic:
intro x y h

Result:
x y : EReal
h : x < y
⊢ x.exp < y.exp
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vadd_eq_vadd_iff_neg_add_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} :
    v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂

Tactic:
rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem mem_doset_of_not_disjoint {H K : Subgroup G} {a b : G}
    (h : ¬Disjoint (doset a H K) (doset b H K)) : b ∈ doset a H K

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Tactic:
refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) ∧ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * b * y
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Tactic:
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ b ∈ doset a ↑H ↑K

Tactic:
rw [Set.not_disjoint_iff] at h

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doset a ↑H ↑K, x ∈ doset b ↑H ↑K
⊢ b ∈ doset a ↑H ↑K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doset a ↑H ↑K, x ∈ doset b ↑H ↑K
⊢ b ∈ doset a ↑H ↑K

Tactic:
simp only [mem_doset] at *

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) ∧ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * b * y
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)

Tactic:
rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.mul_isBigO {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
    (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩

Result:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₂ g₂
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
intro c cpos

Result:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =o[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x

Tactic:
simp only [IsLittleO_def] at *

Result:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₂ g₂
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_nontrivial (h : s.Finite) : h.toFinset.Nontrivial ↔ s.Nontrivial

Proof state:
α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, h.coe_toFinset]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q ≠ 0

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ≠ 0

Tactic:
exact mod_cast ne_of_gt hp.1.pos

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q ≠ 0

Tactic:
rw [padicNorm.eq_zpow_of_nonzero hq]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0

Tactic:
apply zpow_ne_zero

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ≠ 0
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation_neg_orientation (x : E) :
    (-o).rightAngleRotation x = -o.rightAngleRotation x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((-o).areaForm x) y = inner (-o.rightAngleRotation x) y

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((-o).rightAngleRotation x) y = inner (-o.rightAngleRotation x) y

Tactic:
rw [inner_rightAngleRotation_left]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((-o).areaForm x) y = inner (-o.rightAngleRotation x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : E), inner ((-o).rightAngleRotation x) v = inner (-o.rightAngleRotation x) v

Tactic:
intro y

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((-o).rightAngleRotation x) y = inner (-o.rightAngleRotation x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (-o).rightAngleRotation x = -o.rightAngleRotation x

Tactic:
apply ext_inner_right ℝ

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : E), inner ((-o).rightAngleRotation x) v = inner (-o.rightAngleRotation x) v
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_bot : (⊥ : Ideal R).matricesOver n = ⊥

Proof state:
case h.mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
intro H

Result:
case h.mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M ∈ matricesOver n ⊥ ↔ M ∈ ⊥

Tactic:
simp only [mem_matricesOver, mem_bot]

Result:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0

Proof state:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ matricesOver n ⊥ = ⊥

Tactic:
ext M

Result:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M ∈ matricesOver n ⊥ ↔ M ∈ ⊥

Proof state:
case h.mp.a
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i✝ j✝ : n
⊢ M i✝ j✝ = 0 i✝ j✝

Tactic:
apply H

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

case h.mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Proof state:
case h.mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

Tactic:
intro H

Result:
case h.mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0

Proof state:
case h.mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0

Tactic:
simp [H]

Result:
no goals

Proof state:
case h.mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0

Tactic:
ext

Result:
case h.mp.a
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i✝ j✝ : n
⊢ M i✝ j✝ = 0 i✝ j✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
lemma tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) :
    Tendsto (b ^ · : ℝ → ℝ) atBot (𝓝 0)

Proof state:
b : ℝ
hb : 1 < b
⊢ 1 < b

Tactic:
aesop

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 < log b

Tactic:
exact (log_pos_iff (by positivity)).mpr <| by aesop

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => b ^ x) atBot (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Result:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => rexp (log b * x)) atBot (𝓝 0)

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 ≤ b

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : 1 < b
⊢ Tendsto (fun x => rexp (log b * x)) atBot (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_iff_pos <| tendsto_id (α := ℝ)).mpr ?_

Result:
b : ℝ
hb : 1 < b
⊢ 0 < log b

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
positivity

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_filter_lt (a b c : α) : {x ∈ Ico a b | x < c} = Ico a (min b c)

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a (b ⊓ c)

Tactic:
rw [Ico_filter_lt_of_right_le h, min_eq_left h]

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
⊢ filter (fun x => x < c) (Ico a b) = Ico a (b ⊓ c)

Tactic:
rw [Ico_filter_lt_of_le_right h, min_eq_right h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x => x < c) (Ico a b) = Ico a (b ⊓ c)

Tactic:
cases le_total b c with
| inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
| inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
    let assignments := (insertRupUnits f units).fst.assignments
    have hsize : assignments.size = n

Proof state:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i

Tactic:
intro j

Result:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 h,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i

Tactic:
apply Or.inl

Result:
case h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
⊢ f.assignments.size = n

Tactic:
rw [f_readyForRupAdd.2.1]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_Ici : #(Ici a) = n - a

Proof state:
n : ℕ
a : Fin n
⊢ #(Ici a) = n - ↑a

Tactic:
cases n with
| zero => exact Fin.elim0 a
| succ =>
  rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.add_one_sub_one]

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a : Fin (n✝ + 1)
⊢ #(Ici a) = n✝ + 1 - ↑a

Tactic:
rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.add_one_sub_one]

Result:
no goals

Proof state:
case zero
a : Fin 0
⊢ #(Ici a) = 0 - ↑a

Tactic:
exact Fin.elim0 a

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Tor.lean
@[simp]
lemma Tor'_map_app' (n : ℕ) {X Y : C} (f : X ⟶ Y) (Z : C) :
    ((Tor' C n).map f).app Z = (Functor.leftDerived ((tensoringRight C).obj Z) n).map f

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : Abelian C
inst✝¹ : MonoidalPreadditive C
inst✝ : HasProjectiveResolutions C
n : ℕ
X Y : C
f : X ⟶ Y
Z : C
⊢ ((Tor' C n).map f).app Z = (((tensoringRight C).obj Z).leftDerived n).map f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem setOf_indep_eq (M : Matroid α) : {I | M.Indep I} = lowerClosure ({B | M.IsBase B})

Proof state:
α : Type u_1
M : Matroid α
⊢ {I | ∃ B, M.IsBase B ∧ I ⊆ B} = ↑(lowerClosure {B | M.IsBase B})

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ {I | M.Indep I} = ↑(lowerClosure {B | M.IsBase B})

Tactic:
simp_rw [indep_iff]

Result:
α : Type u_1
M : Matroid α
⊢ {I | ∃ B, M.IsBase B ∧ I ⊆ B} = ↑(lowerClosure {B | M.IsBase B})
-- Mathlib/Data/List/FinRange.lean
theorem finRange_succ_eq_map (n : ℕ) : finRange n.succ = 0 :: (finRange n).map Fin.succ

Proof state:
case a
n : ℕ
⊢ map Fin.val (finRange n.succ) = map Fin.val (0 :: map Fin.succ (finRange n))

Tactic:
rw [map_cons, map_coe_finRange, range_succ_eq_map, Fin.val_zero, ← map_coe_finRange, map_map,
  map_map]

Result:
case a
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)

Proof state:
case a
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)

Tactic:
simp only [Function.comp_def, Fin.val_succ]

Result:
no goals

Proof state:
n : ℕ
⊢ finRange n.succ = 0 :: map Fin.succ (finRange n)

Tactic:
apply map_injective_iff.mpr Fin.val_injective

Result:
case a
n : ℕ
⊢ map Fin.val (finRange n.succ) = map Fin.val (0 :: map Fin.succ (finRange n))
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_neg_apply :
    mpullback I I' f (-V) x = - mpullback I I' f V x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
V : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (-V) x = -mpullback I I' f V x

Tactic:
simp [mpullback_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaarMeasure_eq_volume_pi (ι : Type*) [Fintype ι] :
    addHaarMeasure (piIcc01 ι) = volume

Proof state:
case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)

Tactic:
simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk,
  Compacts.coe_mk, Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = volume

Tactic:
convert (addHaarMeasure_unique volume (piIcc01 ι)).symm

Result:
case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)