harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem rank_lt_aleph0 [Module.Finite R M] : Module.rank R M < ℵ₀

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ ⨆ ι, #↑↑ι < ℵ₀

Tactic:
obtain ⟨S, hS⟩ := Module.finite_def.mp ‹Module.Finite R M›

Result:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ⨆ ι, #↑↑ι < ℵ₀

Proof state:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
S : Finset M
hS : span R ↑S = ⊤
i : { s // LinearIndepOn R id s }
⊢ #↑↑i ≤ ↑S.card

Tactic:
exact linearIndependent_le_span_finset _ i.prop S hS

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ Module.rank R M < ℵ₀

Tactic:
simp only [Module.rank_def]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ ⨆ ι, #↑↑ι < ℵ₀

Proof state:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ⨆ ι, #↑↑ι < ℵ₀

Tactic:
refine (ciSup_le' fun i => ?_).trans_lt (nat_lt_aleph0 S.card)

Result:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
S : Finset M
hS : span R ↑S = ⊤
i : { s // LinearIndepOn R id s }
⊢ #↑↑i ≤ ↑S.card
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.mul_sum_of_mem (he : OrthogonalIdempotents e)
    {i : I} {s : Finset I} (h : i ∈ s) : e i * ∑ j ∈ s, e j = e i

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
classical
simp [Finset.mul_sum, he.mul_eq, h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
simp [Finset.mul_sum, he.mul_eq, h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem find_eq_none_iff {n : ℕ} {p : Fin n → Prop} [DecidablePred p] :
    find p = none ↔ ∀ i, ¬p i

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ∀ (i : Fin n), ¬p i

Tactic:
rw [← not_exists, ← isSome_find_iff]

Result:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ¬(find p).isSome = true

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ¬(find p).isSome = true

Tactic:
cases find p <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_zero_iff {z : ℂ} : arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Proof state:
case refine_2.mk
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = 0

Tactic:
rintro ⟨h, rfl : y = 0⟩

Result:
case refine_2.mk.intro
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ { re := x, im := 0 }.arg = 0

Proof state:
case refine_2.mk.intro
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ { re := x, im := 0 }.arg = 0

Tactic:
exact arg_ofReal_of_nonneg h

Result:
no goals

Proof state:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Result:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).re ∧ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).im = 0

Proof state:
z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0

case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Proof state:
case refine_1
z : ℂ
h : z.arg = 0
⊢ 0 ≤ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).re ∧ (↑‖z‖ * (cos ↑0 + sin ↑0 * I)).im = 0

Tactic:
simp [norm_nonneg]

Result:
no goals

Proof state:
case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
obtain ⟨x, y⟩ := z

Result:
case refine_2.mk
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = 0
-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP.go_ne_nil (xs acc : List α) : splitOnP.go p xs acc ≠ []

Proof state:
α : Type u_1
p : α → Bool
xs acc : List α
⊢ go p xs acc ≠ []

Tactic:
induction xs generalizing acc <;> simp [go]

Result:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (acc : List α), go p tail✝ acc ≠ []
acc : List α
⊢ ¬(if p head✝ = true then acc.reverse :: go p tail✝ [] else go p tail✝ (head✝ :: acc)) = []

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (acc : List α), go p tail✝ acc ≠ []
acc : List α
⊢ ¬(if p head✝ = true then acc.reverse :: go p tail✝ [] else go p tail✝ (head✝ :: acc)) = []

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k

Proof state:
case succ.nil
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
h : drop (k + 1) [] = []
⊢ [].length ≤ k + 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
head✝ : α
tail✝ : List α
h : drop (k + 1) (head✝ :: tail✝) = []
⊢ (head✝ :: tail✝).length ≤ k + 1

Tactic:
simp only [drop] at h

Result:
case succ.cons
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
head✝ : α
tail✝ : List α
h : drop k tail✝ = []
⊢ (head✝ :: tail✝).length ≤ k + 1

Proof state:
case succ.cons
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
head✝ : α
tail✝ : List α
h : drop k tail✝ = []
⊢ (head✝ :: tail✝).length ≤ k + 1

Tactic:
simpa [Nat.succ_le_succ_iff] using hk h

Result:
no goals

Proof state:
case zero
α : Type u_1
l : List α
h : drop 0 l = []
⊢ l.length ≤ 0

Tactic:
simp only [drop] at h

Result:
case zero
α : Type u_1
l : List α
h : l = []
⊢ l.length ≤ 0

Proof state:
case zero
α : Type u_1
l : List α
h : l = []
⊢ l.length ≤ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case succ
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
l : List α
h : drop (k + 1) l = []
⊢ l.length ≤ k + 1

Tactic:
cases l

Result:
case succ.nil
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
h : drop (k + 1) [] = []
⊢ [].length ≤ k + 1

case succ.cons
α : Type u_1
k : Nat
hk : ∀ {l : List α}, drop k l = [] → l.length ≤ k
head✝ : α
tail✝ : List α
h : drop (k + 1) (head✝ :: tail✝) = []
⊢ (head✝ :: tail✝).length ≤ k + 1

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ drop k l = [] ↔ l.length ≤ k

Tactic:
refine ⟨fun h => ?_, drop_eq_nil_of_le⟩

Result:
α : Type u_1
l : List α
k : Nat
h : drop k l = []
⊢ l.length ≤ k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd

Proof state:
w : Nat
x y : BitVec w
⊢ x + y = (x.adc y false).snd

Tactic:
simp [adc_spec]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
theorem trace_eq_sum_roots_charpoly_of_splits (hAps : A.charpoly.Splits (RingHom.id R)) :
    A.trace = (Matrix.charpoly A).roots.sum

Proof state:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
⊢ A.trace = A.charpoly.roots.sum

Tactic:
rcases isEmpty_or_nonempty n with h | _

Result:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
h : IsEmpty n
⊢ A.trace = A.charpoly.roots.sum

case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
h✝ : Nonempty n
⊢ A.trace = A.charpoly.roots.sum

Proof state:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
h : IsEmpty n
⊢ A.trace = A.charpoly.roots.sum

Tactic:
rw [Matrix.trace, Fintype.sum_empty, Matrix.charpoly,
  det_eq_one_of_card_eq_zero (Fintype.card_eq_zero_iff.2 h), Polynomial.roots_one,
  Multiset.empty_eq_zero, Multiset.sum_zero]

Result:
no goals

Proof state:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
h✝ : Nonempty n
⊢ A.trace = A.charpoly.roots.sum

Tactic:
rw [trace_eq_neg_charpoly_coeff, neg_eq_iff_eq_neg,
  ← Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split A.charpoly_monic hAps, nextCoeff,
  charpoly_natDegree_eq_dim, if_neg (Fintype.card_ne_zero : Fintype.card n ≠ 0)]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_nat (n : ℕ) :
    HasDerivAt Gamma (n ! * (-γ + harmonic n)) (n + 1)

Proof state:
n : ℕ
⊢ DifferentiableAt ℂ Gamma ↑(↑n + 1)

Tactic:
exact_mod_cast differentiable_at_Gamma_nat_add_one n

Result:
no goals

Proof state:
n : ℕ
⊢ HasDerivAt Gamma (↑n ! * (-↑γ + ↑(harmonic n))) (↑n + 1)

Tactic:
exact_mod_cast HasDerivAt.complex_of_real
  (by exact_mod_cast differentiable_at_Gamma_nat_add_one n)
  (Real.hasDerivAt_Gamma_nat n) Gamma_ofReal

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v : V
x : P
⊢ dist (v +ᵥ x) x = ‖v‖

Tactic:
simp [dist_eq_norm_vsub V _ x]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.orthogonal_orthogonal_eq_closure [CompleteSpace E] :
    Kᗮᗮ = K.topologicalClosure

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = K.topologicalClosure

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ ≤ K.topologicalClosure

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure ≤ Kᗮᗮ

Proof state:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = K.topologicalClosureᗮᗮ

Tactic:
rw [K.topologicalClosure.orthogonal_orthogonal]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ ≤ K.topologicalClosure

Tactic:
convert Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure using 1

Result:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = K.topologicalClosureᗮᗮ

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure ≤ Kᗮᗮ

Tactic:
exact K.topologicalClosure_minimal K.le_orthogonal_orthogonal Kᗮ.isClosed_orthogonal

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_zpow_neg_valuation {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = (p : ℝ) ^ (-x.valuation)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ‖Quotient.mk'' f‖ = ↑p ^ (-valuation (Quotient.mk'' f))

Tactic:
change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f ≈ 0

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero

Result:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f - 0 ≈ 0

Proof state:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ Quotient.mk'' f = 0

Tactic:
apply Quotient.sound

Result:
case hf.a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ f ≈ const (padicNorm p) 0

Proof state:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ False

Tactic:
apply hf

Result:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ Quotient.mk'' f = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)

Tactic:
rw [PadicSeq.norm_eq_zpow_neg_valuation]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)

p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f ≈ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)

Tactic:
rw [Rat.cast_zpow, Rat.cast_natCast]

Result:
no goals

Proof state:
case hf.a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ f ≈ const (padicNorm p) 0

Tactic:
simpa using hf'

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

Tactic:
refine Quotient.inductionOn' x fun f hf => ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ‖Quotient.mk'' f‖ = ↑p ^ (-valuation (Quotient.mk'' f))

Proof state:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f - 0 ≈ 0

Tactic:
intro hf'

Result:
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c

Proof state:
a b c : Int
h : a + b < a + c
⊢ b < c

Tactic:
have : -a + (a + b) < -a + (a + c) := Int.add_lt_add_left h _

Result:
a b c : Int
h : a + b < a + c
this : -a + (a + b) < -a + (a + c)
⊢ b < c

Proof state:
a b c : Int
h : a + b < a + c
this : -a + (a + b) < -a + (a + c)
⊢ b < c

Tactic:
simp [Int.neg_add_cancel_left] at this

Result:
a b c : Int
h : a + b < a + c
this : b < c
⊢ b < c

Proof state:
a b c : Int
h : a + b < a + c
this : b < c
⊢ b < c

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR

Proof state:
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ (match f a with
    | none => acc.toList ++ filterMap f as
    | some b => acc.toList ++ b :: filterMap f as) =
    acc.toList ++
      match f a with
      | none => filterMap f as
      | some b => b :: filterMap f as

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
acc : Array β
⊢ filterMapTR.go f [] acc = acc.toList ++ filterMap f []

Tactic:
simp [filterMapTR.go, filterMap]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ filterMapTR.go f (a :: as) acc = acc.toList ++ filterMap f (a :: as)

Tactic:
simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
  filterMap]

Result:
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
a : α
as : List α
acc : Array β
⊢ (match f a with
    | none => acc.toList ++ filterMap f as
    | some b => acc.toList ++ b :: filterMap f as) =
    acc.toList ++
      match f a with
      | none => filterMap f as
      | some b => b :: filterMap f as

Proof state:
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l

Tactic:
exact (go l #[]).symm

Result:
no goals

Proof state:
⊢ @filterMap = @filterMapTR

Tactic:
funext α β f l

Result:
case h.h.h.h
α : Type u_2
β : Type u_1
f : α → Option β
l : List α
⊢ filterMap f l = filterMapTR f l
-- Mathlib/Data/ENNReal/Basic.lean
theorem iUnion_Ioo_coe_nat : ⋃ n : ℕ, Ioo a n = Ioi a \ {∞}

Proof state:
a : ℝ≥0∞
⊢ ⋃ n, Ioo a ↑n = Ioi a \ {⊤}

Tactic:
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_finrank_top (h : A ≤ B) : relfinrank A B * finrank B E = finrank A E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank B * finrank (↥B) E = finrank (↥A) E

Tactic:
simpa using congr(toNat $(relrank_mul_rank_top h))

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_toReal_iff {ι} {fi : Filter ι} {f : ι → ℝ≥0∞} (hf : ∀ i, f i ≠ ∞) {x : ℝ≥0∞}
    (hx : x ≠ ∞) : Tendsto (fun n => (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x)

Proof state:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ Tendsto (fun n => (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x)

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case intro
ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ⊤
f : ι → ℝ≥0
⊢ Tendsto (fun n => ((fun i => ↑(f i)) n).toReal) fi (𝓝 x.toReal) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 x)

Proof state:
case intro
ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ⊤
f : ι → ℝ≥0
⊢ Tendsto (fun n => ((fun i => ↑(f i)) n).toReal) fi (𝓝 x.toReal) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 x)

Tactic:
lift x to ℝ≥0 using hx

Result:
case intro.intro
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n => ((fun i => ↑(f i)) n).toReal) fi (𝓝 (↑x).toReal) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 ↑x)

Proof state:
case intro.intro
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n => ((fun i => ↑(f i)) n).toReal) fi (𝓝 (↑x).toReal) ↔ Tendsto (fun i => ↑(f i)) fi (𝓝 ↑x)

Tactic:
simp [tendsto_coe]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_concat
    (f : β → α → β) (b : β) (x : α) (xs : List α) :
    List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x

Proof state:
α : Type u
β : Type v
f : β → α → β
b : β
x : α
xs : List α
⊢ foldl f b (xs ++ [x]) = f (foldl f b xs) x

Tactic:
simp only [List.foldl_append, List.foldl]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem iSup_toSubsemiring {ι : Sort*} [Nonempty ι] (S : ι → Subalgebra R A) :
    (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
⊢ (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring

Tactic:
simp only [iSup, Set.range_nonempty, sSup_toSubsemiring, ← Set.range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem induction_on {M : R[T;T⁻¹] → Prop} (p : R[T;T⁻¹]) (h_C : ∀ a, M (C a))
    (h_add : ∀ {p q}, M p → M q → M (p + q))
    (h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T n) → M (C a * T (n + 1)))
    (h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-n)) → M (C a * T (-n - 1))) : M p

Proof state:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.toFun n) * T n)

Tactic:
apply Finset.induction

Result:
case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ M (∑ n ∈ ∅, C (p.toFun n) * T n)

case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ ⦃a : ℤ⦄ {s : Finset ℤ}, a ∉ s → M (∑ n ∈ s, C (p.toFun n) * T n) → M (∑ n ∈ insert a s, C (p.toFun n) * T n)
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
lemma disjiUnion_supp_toFinset_eq_supp_toFinset {G' : SimpleGraph V} (h : G ≤ G')
    (c' : ConnectedComponent G') [Fintype c'.supp]
    [DecidablePred fun c : G.ConnectedComponent ↦ c.supp ⊆ c'.supp] :
    .disjiUnion {c : ConnectedComponent G | c.supp ⊆ c'.supp} (fun c ↦ c.supp.toFinset)
      (fun x _ y _ hxy ↦ by simpa using pairwise_disjoint_supp_connectedComponent _ hxy) =
      c'.supp.toFinset :=
  Finset.coe_injective <| by simpa using ConnectedComponent.biUnion_supp_eq_supp h _

Proof state:
V : Type u
G : SimpleGraph V
inst✝⁴ : DecidableEq V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst✝¹ : Fintype ↑c'.supp
inst✝ : DecidablePred fun c => c.supp ⊆ c'.supp
x : G.ConnectedComponent
x✝¹ : x ∈ ↑(filter (fun c => c.supp ⊆ c'.supp) univ)
y : G.ConnectedComponent
x✝ : y ∈ ↑(filter (fun c => c.supp ⊆ c'.supp) univ)
hxy : x ≠ y
⊢ (Disjoint on fun c => c.supp.toFinset) x y

Tactic:
simpa using pairwise_disjoint_supp_connectedComponent _ hxy

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝⁴ : DecidableEq V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst✝¹ : Fintype ↑c'.supp
inst✝ : DecidablePred fun c => c.supp ⊆ c'.supp
⊢ ↑((filter (fun c => c.supp ⊆ c'.supp) univ).disjiUnion (fun c => c.supp.toFinset) ⋯) = ↑c'.supp.toFinset

Tactic:
simpa using ConnectedComponent.biUnion_supp_eq_supp h _

Result:
no goals