harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem zero_lt_card {o} : 0 < card o ↔ 0 < o

Proof state:
o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o

Tactic:
simpa using nat_lt_card (n := 0)

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem symm_proj_apply (e : Pretrivialization F (π F E)) (z : TotalSpace F E)
    (hz : z.proj ∈ e.baseSet) : e.symm z.proj (e z).2 = z.2

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → Zero (E x)
e : Pretrivialization F TotalSpace.proj
z : TotalSpace F E
hz : z.proj ∈ e.baseSet
⊢ e.symm z.proj (↑e z).2 = z.snd

Tactic:
rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_eq_empty_iff {σ : Perm α} : σ.support = ∅ ↔ σ = 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ.support = ∅ ↔ σ = 1

Tactic:
simp_rw [Finset.ext_iff, mem_support, Finset.not_mem_empty, iff_false, not_not,
  Equiv.Perm.ext_iff, one_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem _root_.Filter.HasBasis.vitaliFamily {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (h : (𝓝 x).HasBasis p s) : (v.filterAt x).HasBasis p (fun i ↦ {t ∈ v.setsAt x | t ⊆ s i})

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ (v.filterAt x).HasBasis p fun i => {t | t ∈ v.setsAt x ∧ t ⊆ s i}

Tactic:
simpa only [← Set.setOf_inter_eq_sep] using h.smallSets.inf_principal _

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_eq_sign (n : ℤ) : Int.sign n = SignType.sign n

Proof state:
n : ℤ
⊢ n.sign = ↑(SignType.sign n)

Tactic:
obtain (n | _) | _ := n <;> simp [sign, Int.sign_neg, negSucc_lt_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernel.lift_map {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel g] (w : f ≫ g = 0)
    (f' : X' ⟶ Y') (g' : Y' ⟶ Z') [HasKernel g'] (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y')
    (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
    kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w'

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst✝ : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ (lift g f w ≫ map g g' q r h₂) ≫ equalizer.ι g' 0 = (p ≫ lift g' f' w') ≫ equalizer.ι g' 0

Tactic:
simp [h₁]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst✝ : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ lift g f w ≫ map g g' q r h₂ = p ≫ lift g' f' w'

Tactic:
ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst✝ : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ (lift g f w ≫ map g g' q r h₂) ≫ equalizer.ι g' 0 = (p ≫ lift g' f' w') ≫ equalizer.ι g' 0
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem Span.finsupp_linearCombination_repr {w : Set M} (x : span R w) :
    Finsupp.linearCombination R ((↑) : w → M) (Span.repr R w x) = x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) ⋯.choose = ↑x

Tactic:
exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) (repr R w x) = ↑x

Tactic:
rw [Span.repr_def]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : Set M
x : ↥(span R w)
⊢ (linearCombination R Subtype.val) ⋯.choose = ↑x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y

Proof state:
case mpr
n : Nat
x y : BitVec n
h : x ≠ y
h_eq : x.toNat = y.toNat
⊢ False

Tactic:
apply h <| eq_of_toNat_eq h_eq

Result:
no goals

Proof state:
case mp
n : Nat
x y : BitVec n
⊢ x.toNat ≠ y.toNat → x ≠ y

Tactic:
rintro h rfl

Result:
case mp
n : Nat
x : BitVec n
h : x.toNat ≠ x.toNat
⊢ False

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat ≠ y.toNat ↔ x ≠ y

Tactic:
constructor

Result:
case mp
n : Nat
x y : BitVec n
⊢ x.toNat ≠ y.toNat → x ≠ y

case mpr
n : Nat
x y : BitVec n
⊢ x ≠ y → x.toNat ≠ y.toNat

Proof state:
case mp
n : Nat
x : BitVec n
h : x.toNat ≠ x.toNat
⊢ False

Tactic:
apply h rfl

Result:
no goals

Proof state:
case mpr
n : Nat
x y : BitVec n
⊢ x ≠ y → x.toNat ≠ y.toNat

Tactic:
intro h h_eq

Result:
case mpr
n : Nat
x y : BitVec n
h : x ≠ y
h_eq : x.toNat = y.toNat
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem _root_.Complex.Gamma_ofReal (s : ℝ) : Complex.Gamma (s : ℂ) = Gamma s

Proof state:
s : ℝ
⊢ Complex.Gamma ↑s = ↑(Gamma s)

Tactic:
rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem entries_insert_of_not_mem {a : α} {b : β a} {s : Finmap β} :
    a ∉ s → (insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries :=
  induction_on s fun s h => by
    -- Porting note: `-entries_insert` required
    simp [AList.entries_insert_of_not_mem (mt mem_toFinmap.1 h), -entries_insert]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
h : a ∉ ⟦s⟧
⊢ (insert a b ⟦s⟧).entries = ⟨a, b⟩ ::ₘ ⟦s⟧.entries

Tactic:
simp [AList.entries_insert_of_not_mem (mt mem_toFinmap.1 h), -entries_insert]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem map [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x)

Proof state:
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit (f x)

Tactic:
rcases h with ⟨y, rfl⟩

Result:
case intro
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (f ↑y)

Proof state:
case intro
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : FunLike F M N
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (f ↑y)

Tactic:
exact (Units.map (f : M →* N) y).isUnit

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l.tail
⊢ a ∈ l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_le_iSup {ι : Type u} (f : ι → Cardinal.{u}) : sum f ≤ #ι * iSup f

Proof state:
ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * iSup f

Tactic:
rw [← lift_id #ι]

Result:
ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ lift.{u, u} #ι * iSup f

Proof state:
ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ lift.{u, u} #ι * iSup f

Tactic:
exact sum_le_iSup_lift f

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeffsIn_pow : ∀ {n}, n ≠ 0 → ∀ M : Submodule R S, coeffsIn σ (M ^ n) = coeffsIn σ M ^ n
  | 1, _, M => by simp
  | n + 2, _, M => by rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]; exact n.succ_ne_zero

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ coeffsIn σ (M ^ (n + 2)) = coeffsIn σ M ^ (n + 2)

Tactic:
rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]

Result:
case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Proof state:
case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
exact n.succ_ne_zero

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : 1 ≠ 0
M : Submodule R S
⊢ coeffsIn σ (M ^ 1) = coeffsIn σ M ^ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem lieSpan_eq_bot_iff : lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = (0 : M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0

Tactic:
rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem eqOn_closure_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : IsBounded U)
    (hf : DiffContOnCl ℂ f U) (hg : DiffContOnCl ℂ g U) (hfg : EqOn f g (frontier U)) :
    EqOn f g (closure U)

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
z : E
hz : z ∈ closure U
w : E
hw : w ∈ frontier U
⊢ ‖(f - g) w‖ ≤ 0

Tactic:
simp [hfg hw]

Result:
no goals

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure U)

Tactic:
simpa [sub_eq_zero] using H

Result:
no goals

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ EqOn f g (closure U)

Tactic:
suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0 by simpa [sub_eq_zero] using H

Result:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0

Tactic:
refine fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz

Result:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
z : E
hz : z ∈ closure U
w : E
hw : w ∈ frontier U
⊢ ‖(f - g) w‖ ≤ 0
-- Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
theorem sum_boxes_congr [Finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π₁ π₂ : Prepartition I}
    (h : π₁.iUnion = π₂.iUnion) : ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Proof state:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
clear hs

Result:
case intro
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J => splitMany J s) = (splitMany I s).filter fun J => ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
-- Mathlib/Analysis/RCLike/Inner.lean
lemma linearIndependent_of_ne_zero_of_wInner_one_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0) : LinearIndependent 𝕜 f

Proof state:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => wInner 1 (f k₁) (f k₂) = 0
⊢ LinearIndependent 𝕜 f

Tactic:
simp_rw [wInner_one_eq_inner] at hinner

Result:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
⊢ LinearIndependent 𝕜 f

Proof state:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
⊢ LinearIndependent 𝕜 f

Tactic:
have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner

Result:
case refine_2
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
this : LinearIndependent 𝕜 fun i => (WithLp.equiv 2 (ι → 𝕜)).symm (f i)
⊢ LinearIndependent 𝕜 f

case refine_1
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
⊢ ∀ (i : κ), (WithLp.equiv 2 (ι → 𝕜)).symm (f i) ≠ 0

Proof state:
case refine_2
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
this : LinearIndependent 𝕜 fun i => (WithLp.equiv 2 (ι → 𝕜)).symm (f i)
⊢ LinearIndependent 𝕜 f

case refine_1
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ => inner ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₁)) ((WithLp.equiv 2 (ι → 𝕜)).symm (f k₂)) = 0
⊢ ∀ (i : κ), (WithLp.equiv 2 (ι → 𝕜)).symm (f i) ≠ 0

Tactic:
exacts [this, hf]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem mem_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
    p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
  ← and_or_left]

Result:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)

Tactic:
simpa only [and_congr_right_iff] using Prime.dvd_mul

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b

Proof state:
a : Int
b : Nat
h : 0 < a
⊢ 0 < a ^ b

Tactic:
rw [Int.eq_natAbs_of_zero_le (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt]

Result:
a : Int
b : Nat
h : 0 < a
⊢ 0 < a.natAbs ^ b

Proof state:
a : Int
b : Nat
h : 0 < a
⊢ 0 < a.natAbs ^ b

Tactic:
exact Nat.pos_pow_of_pos _ (Int.natAbs_pos.mpr (Int.ne_of_gt h))

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma sign_cases_of_C_mul_pow_nonneg [PosMulStrictMono α]
    (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
ha : 0 < a
⊢ 0 ≤ a * b

Tactic:
simpa only [pow_one] using h 1

Result:
no goals

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0

Result:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ 0 ≤ a

Tactic:
simpa only [pow_zero, mul_one] using h 0

Result:
no goals

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
refine this.eq_or_gt.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩

Result:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
a b : α
inst✝ : PosMulStrictMono α
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
ha : 0 < a
⊢ 0 ≤ a * b
-- Mathlib/Data/Matrix/Mul.lean
theorem one_vecMul [Fintype m] (A : Matrix m n α) : 1 ᵥ* A = ∑ i, A i

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ 1 ᵥ* A = ∑ i : m, A i

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (1 ᵥ* A) x✝ = (∑ i : m, A i) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (1 ᵥ* A) x✝ = (∑ i : m, A i) x✝

Tactic:
simp [vecMul, dotProduct]

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

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

Tactic:
simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
  restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]

Result:
α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)

Proof state:
α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapHomologyIso_inv_naturality [S₁.HasHomology] [S₂.HasHomology]
    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv =
      (S₁.mapHomologyIso F).inv ≫
      @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv = (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k) (hr' : r'.coeff 0 ≠ 0)
    (hq' : q'.coeff 0 ≠ 0) (hq : (p : 𝕎 k) ^ n * q' ∈ nonZeroDivisors (𝕎 k)) :
    let b : 𝕎 k := frobeniusRotation p hr' hq'
    IsFractionRing.ringEquivOfRingEquiv (frobeniusEquiv p k)
          (algebraMap (𝕎 k) (FractionRing (𝕎 k)) b) *
        Localization.mk ((p : 𝕎 k) ^ m * r') ⟨(p : 𝕎 k) ^ n * q', hq⟩ =
      (p : Localization (nonZeroDivisors (𝕎 k))) ^ (m - n : ℤ) *
        algebraMap (𝕎 k) (FractionRing (𝕎 k)) b

Proof state:
case h.e'_3
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * ↑p ^ m * r' * ↑p ^ n = ↑p ^ m * b * (↑p ^ n * q')
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ ↑p ^ m * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b * (↑p ^ n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q') =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k))) (↑p ^ m * b * (↑p ^ n * q'))

Tactic:
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma rightHomologyMap_op (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
    (rightHomologyMap φ).op = S₂.leftHomologyOpIso.inv ≫ leftHomologyMap (opMap φ) ≫
      S₁.leftHomologyOpIso.hom

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (rightHomologyMap φ).op = S₂.leftHomologyOpIso.inv ≫ leftHomologyMap (opMap φ) ≫ S₁.leftHomologyOpIso.hom

Tactic:
dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap,
  rightHomologyMap]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData).op =
    leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData ≫
      leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData ≫
        leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData).op =
    leftHomologyMap' (𝟙 S₂.op) S₂.rightHomologyData.op S₂.op.leftHomologyData ≫
      leftHomologyMap' (opMap φ) S₂.op.leftHomologyData S₁.op.leftHomologyData ≫
        leftHomologyMap' (𝟙 S₁.op) S₁.op.leftHomologyData S₁.rightHomologyData.op

Tactic:
simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]

Result:
no goals