harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive]
lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
  | 1, _ => by simp
  | n + 2, _ =>
    calc
      closure (s ^ (n + 2))
      _ = closure (s ^ (n + 1) * s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 2)) = closure (s ^ (n + 1) * s)

Tactic:
rw [pow_succ]

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ⊔ closure s ≤ closure s ⊔ closure s

Tactic:
gcongr ?_ ⊔ _

Result:
case h₁
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ≤ closure s

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
x✝ : 1 ≠ 0
⊢ closure (s ^ 1) ≤ closure s

Tactic:
simp

Result:
no goals

Proof state:
case h₁
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ≤ closure s

Tactic:
exact closure_pow_le n.succ_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn_id_yield_eq_elim
    (o : Option α) (f : (a : α) → β → β) (b : β) :
    forIn (m := Id) o b (fun a b => .yield (f a b)) =
      o.elim b (fun a => f a b)

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → β → β
b : β
⊢ (forIn o b fun a b => ForInStep.yield (f a b)) = o.elim b fun a => f a b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_le_rpow {x z : ℝ} (hx : 1 ≤ x) (hz : 0 ≤ z) : 1 ≤ x ^ z

Proof state:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z

Tactic:
exact rpow_le_rpow zero_le_one hx hz

Result:
no goals

Proof state:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z

Tactic:
rw [← one_rpow z]

Result:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z
-- Mathlib/Data/List/AList.lean
theorem insertRec_empty {C : AList β → Sort*} (H0 : C ∅)
    (IH : ∀ (a : α) (b : β a) (l : AList β), a ∉ l → C l → C (l.insert a b)) :
    @insertRec α β _ C H0 IH ∅ = H0

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)
⊢ insertRec H0 IH ∅ = H0

Tactic:
change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)
⊢ insertRec H0 IH { entries := [], nodupKeys := ⋯ } = H0

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)
⊢ insertRec H0 IH { entries := [], nodupKeys := ⋯ } = H0

Tactic:
rw [insertRec]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_inter_ground_eq (I E : Set α) :
    uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

Proof state:
α : Type u_1
I E : Set α
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
I E : Set α
⊢ uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

Tactic:
simp only [uniqueBaseOn, restrict_eq_restrict_iff, freeOn_indep_iff, subset_inter_iff,
  iff_self_and]

Result:
α : Type u_1
I E : Set α
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atBot ↔ r < 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atBot ↔ r < 0

Tactic:
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n = 1 ↔ x = 1

Tactic:
simp only [le_antisymm_iff]

Result:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x

Tactic:
rw [pow_le_one_iff hn, one_le_pow_iff hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Entails α σ1]
    [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
    Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_eq_f2 : Liff α f1 f2
f2_eq_f3 : Liff α f2 f3
a : α → Bool
⊢ a ⊨ f1 ↔ a ⊨ f3

Tactic:
rw [f1_eq_f2 a, f2_eq_f3 a]

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3

Tactic:
intros f1_eq_f2 f2_eq_f3 a

Result:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : Entails α σ1
inst✝¹ : Entails α σ2
inst✝ : Entails α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_eq_f2 : Liff α f1 f2
f2_eq_f3 : Liff α f2 f3
a : α → Bool
⊢ a ⊨ f1 ↔ a ⊨ f3
-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_ι_mul (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M)
    (x : ExteriorAlgebra R M) :
    liftAlternating (R := R) (M := M) (N := N) f (ι R m * x) =
    liftAlternating (R := R) (M := M) (N := N) (fun i => (f i.succ).curryLeft m) x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯)
          (((LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f))
        x 0)
      0 =
    (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x
        0)
      0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m * x) 0) 0 =
    (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x
        0)
      0

Tactic:
rw [foldl_mul, foldl_ι]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯)
          (((LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f))
        x 0)
      0 =
    (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x
        0)
      0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (liftAlternating f) ((ι R) m * x) = (liftAlternating fun i => (f i.succ).curryLeft m) x

Tactic:
dsimp [liftAlternating]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m * x) 0) 0 =
    (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x
        0)
      0
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_right_add_right (m n k : ℕ) : gcd m (k * m + n) = gcd m n

Proof state:
m n k : ℕ
⊢ m.gcd (k * m + n) = m.gcd n

Tactic:
simp [add_comm _ n]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_C_mul_X_pow (x : R) (k n : ℕ) :
    coeff (C x * X ^ k : R[X]) n = if n = k then x else 0

Proof state:
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (C x * X ^ k).coeff n = if n = k then x else 0

Tactic:
rw [C_mul_X_pow_eq_monomial, coeff_monomial]

Result:
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0

Proof state:
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0

Tactic:
congr 1

Result:
case e_c
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (k = n) = (n = k)

Proof state:
case e_c
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (k = n) = (n = k)

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_ofHom {p : ℤ} (φ : F ⟶ G) : δ 0 p (Cochain.ofHom φ) = 0

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ δ 0 1 (Cochain.ofHom φ) = 0

Tactic:
ext

Result:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p✝ q✝ : ℤ
hpq✝ : p✝ + 1 = q✝
⊢ (δ 0 1 (Cochain.ofHom φ)).v p✝ q✝ hpq✝ = Cochain.v 0 p✝ q✝ hpq✝

Proof state:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p✝ q✝ : ℤ
hpq✝ : p✝ + 1 = q✝
⊢ (δ 0 1 (Cochain.ofHom φ)).v p✝ q✝ hpq✝ = Cochain.v 0 p✝ q✝ hpq✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
by_cases h : p = 1

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
rw [δ_shape]

Result:
case neg.hnm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ ¬0 + 1 = p

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
subst h

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ δ 0 1 (Cochain.ofHom φ) = 0

Proof state:
case neg.hnm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : ¬p = 1
⊢ ¬0 + 1 = p

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFreeOn_two : G.CliqueFreeOn s 2 ↔ s.Pairwise (G.Adjᶜ)

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2

Tactic:
simp only [CliqueFreeOn, isNClique_iff, card_eq_two, coe_subset, not_and, not_exists]

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → ∀ ⦃t : Finset α⦄, ↑t ⊆ s → G.IsClique ↑t → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ {a, b} ⊆ s

Tactic:
exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ

Tactic:
refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s

case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → ∀ ⦃t : Finset α⦄, ↑t ⊆ s → G.IsClique ↑t → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}

Tactic:
rintro h t hst ht a b hab rfl

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
hst : ↑{a, b} ⊆ s
ht : G.IsClique ↑{a, b}
⊢ False

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
hst : ↑{a, b} ⊆ s
ht : G.IsClique ↑{a, b}
⊢ False

Tactic:
simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst

Result:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ False

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ False

Tactic:
refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
simpa [hab.ne]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s

Tactic:
push_cast

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ {a, b} ⊆ s
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_top : ∂ (⊤ : α) = ⊥

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ∂ ⊤ = ⊥

Tactic:
rw [boundary, hnot_top, inf_bot_eq]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma toCLM_apply_eq_sum {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ (n → A)} :
    toCLM M v = (WithCStarModule.equiv _).symm (fun i => ∑ j, M i j * v j)

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
⊢ (toCLM M) v i = (WithCStarModule.equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i

Tactic:
simp [toCLM_apply, Matrix.mulVec, dotProduct]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ (toCLM M) v = (WithCStarModule.equiv (m → A)).symm fun i => ∑ j : n, M i j * v j

Tactic:
ext i

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
⊢ (toCLM M) v i = (WithCStarModule.equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i
-- Mathlib/Data/Set/Pairwise/Lattice.lean
lemma Set.pairwiseDisjoint_iff :
    s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
  not_disjoint_iff_nonempty_inter]

Result:
no goals
-- Mathlib/Order/Max.lean
theorem IsBot.not_isMax [Nontrivial α] (ha : IsBot a) : ¬ IsMax a

Proof state:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False

Tactic:
exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_ne a

Result:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
⊢ ¬IsMax a

Tactic:
intro ha'

Result:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
⊢ False
-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
theorem toStalk_comp_stalkToFiberLinearMap (x : PrimeSpectrum.Top R) :
    toStalk M x ≫ stalkToFiberLinearMap M x =
    ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen M ⊤ ≫ openToLocalization M ⊤ x True.intro = ↟(LocalizedModule.mkLinearMap x.asIdeal.primeCompl ↑M)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
⊢ toStalk M x ≫ stalkToFiberLinearMap M x = ↟(LocalizedModule.mkLinearMap x.asIdeal.primeCompl ↑M)

Tactic:
rw [toStalk, Category.assoc, germ_comp_stalkToFiberLinearMap]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen M ⊤ ≫ openToLocalization M ⊤ x True.intro = ↟(LocalizedModule.mkLinearMap x.asIdeal.primeCompl ↑M)
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem opRingEquiv_symm_single [Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
r : kᵐᵒᵖ
x : Gᵐᵒᵖ
⊢ MonoidAlgebra.opRingEquiv.symm (single x r) = op (single (unop x) (unop r))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
    (as.modify i f)[i] = f (as[i]'(by simpa using h))

Proof state:
α : Type u_1
as : Array α
i : Nat
f : α → α
h : i < (as.modify i f).size
⊢ (as.modify i f)[i] = f as[i]

Tactic:
simp [getElem_modify h]

Result:
no goals

Proof state:
α : Type ?u.512913
as : Array α
i : Nat
f : α → α
h : i < (as.modify i f).size
⊢ i < as.size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_self : trace R R = LinearMap.id

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
⊢ (trace R R) 1 = LinearMap.id 1

Tactic:
simpa using trace_algebraMap_of_basis (.singleton (Fin 1) R) 1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ trace R R = LinearMap.id

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommRing R
⊢ (trace R R) 1 = LinearMap.id 1
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
/-- Specialization of `Finset.prod_nbij'` that automatically fills in most arguments.

See `Fintype.prod_equiv` for the version where `s` and `t` are `univ`. -/
@[to_additive "`Specialization of `Finset.sum_nbij'` that automatically fills in most arguments.

See `Fintype.sum_equiv` for the version where `s` and `t` are `univ`."]
lemma prod_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
    ∏ i ∈ s, f i = ∏ i ∈ t, g i

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ i ∈ t, g i

Tactic:
refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_of_not_mem_support {f : α →₀ M} {a} (haf : a ∉ f.support) : erase a f = f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
⊢ erase a f = f

Tactic:
ext b

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
⊢ (erase a f) b = f b

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
⊢ (erase a f) b = f b

Tactic:
by_cases hab : b = a

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
hab : b = a
⊢ (erase a f) b = f b

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
hab : ¬b = a
⊢ (erase a f) b = f b

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
hab : ¬b = a
⊢ (erase a f) b = f b

Tactic:
rw [erase_ne hab]

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
haf : a ∉ f.support
b : α
hab : b = a
⊢ (erase a f) b = f b

Tactic:
rwa [hab, erase_same, eq_comm, ← not_mem_support_iff]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem pair_lt_pair_right (a) {b₁ b₂} (h : b₁ < b₂) : pair a b₁ < pair a b₂

Proof state:
case pos.h
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ ≤ a + a

Tactic:
exact le_trans h₁ (Nat.le_add_left _ _)

Result:
no goals

Proof state:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Tactic:
simp? at h₁ says simp only [not_lt] at h₁

Result:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Proof state:
a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by_cases h₁ : a < b₁

Result:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂

Proof state:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h

Result:
no goals

Proof state:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Tactic:
rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]

Result:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ + a * a < b₂ * b₂

Proof state:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Result:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Proof state:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Tactic:
simp only [not_lt] at h₁

Result:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Proof state:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
by_cases h₂ : a < b₂ <;> simp [pair, h₂, h]

Result:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Proof state:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ + a * a < b₂ * b₂

Tactic:
rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]

Result:
case pos.h
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ ≤ a + a