harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_range [Finite ι] : LinearMap.range b.toDual = ⊤

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ range b.toDual = ⊤

Tactic:
refine eq_top_iff'.2 fun f => ?_

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
⊢ f ∈ range b.toDual

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) lin_comb)) (b i) = f (b i)

Tactic:
rw [b.toDual_eq_repr _ i, repr_linearCombination b]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
i : ι
⊢ lin_comb i = f (b i)

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
⊢ f ∈ range b.toDual

Tactic:
refine ⟨Finsupp.linearCombination R b lin_comb, b.ext fun i => ?_⟩

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) lin_comb)) (b i) = f (b i)

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
⊢ f ∈ range b.toDual

Tactic:
let lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
⊢ f ∈ range b.toDual

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : Dual R M
lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)
i : ι
⊢ lin_comb i = f (b i)

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem mem_support_iff_of_commute {g c : Perm α} (hgc : Commute g c) (x : α) :
    x ∈ c.support ↔ g x ∈ c.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ x ∈ c.support ↔ g x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not, ← mul_apply]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ (c * g) x = g x

Tactic:
rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
    m.contains a = true → m.getKey? a = some (m.getKey! a)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ m.contains a = true → m.getKey? a = some (m.getKey! a)

Tactic:
simp_to_model using List.getKey?_eq_some_getKey!

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
    (h : stop = l.toArray.size) :
    l.toArray.allM p 0 stop = l.allM p

Proof state:
m : Type → Type u_1
α : Type u_2
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
h : stop = l.toArray.size
⊢ allM p l.toArray 0 stop = List.allM p l

Tactic:
subst h

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ allM p l.toArray = List.allM p l

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ allM p l.toArray = List.allM p l

Tactic:
rw [← allM_toList]

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem nilpotent_iff_mem_maximal_of_minimal {x : _} :
    IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal (Localization I.primeCompl)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : I ∈ minimalPrimes R
x : Localization I.primeCompl
⊢ IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal (Localization I.primeCompl)

Tactic:
rw [nilpotent_iff_mem_prime]

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : I ∈ minimalPrimes R
x : Localization I.primeCompl
⊢ (∀ (J : Ideal (Localization I.primeCompl)), J.IsPrime → x ∈ J) ↔
    x ∈ IsLocalRing.maximalIdeal (Localization I.primeCompl)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : I ∈ minimalPrimes R
x : Localization I.primeCompl
x✝¹ : x ∈ IsLocalRing.maximalIdeal (Localization I.primeCompl)
J : Ideal (Localization I.primeCompl)
x✝ : J.IsPrime
⊢ x ∈ J

Tactic:
simpa [prime_unique_of_minimal hMin J]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_bddBelow (x : R) :
    BddBelow (Set.range (seminormFromConst_seq c f x))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ 0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))

Tactic:
rintro r ⟨n, rfl⟩

Result:
case h.intro
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
n : ℕ
⊢ 0 ≤ seminormFromConst_seq c f x n

Proof state:
case h.intro
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
n : ℕ
⊢ 0 ≤ seminormFromConst_seq c f x n

Tactic:
exact seminormFromConst_seq_nonneg c f x n

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ BddBelow (Set.range (seminormFromConst_seq c f x))

Tactic:
use 0

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ 0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))
-- Mathlib/Algebra/Divisibility/Units.lean
theorem dvd_mul_left : a ∣ u * b ↔ a ∣ b

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
rw [mul_comm]

Result:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem eqToHom_c_app {X Y : Scheme} (e : X = Y) (U) :
    (eqToHom e).app U = eqToHom (by subst e; rfl)

Proof state:
X : Scheme
U : X.Opens
⊢ Hom.app (eqToHom ⋯) U = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
subst e

Result:
X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)

Proof state:
X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Hom.app (eqToHom e) U = eqToHom ⋯

Tactic:
subst e

Result:
X : Scheme
U : X.Opens
⊢ Hom.app (eqToHom ⋯) U = eqToHom ⋯
-- Mathlib/LinearAlgebra/Contraction.lean
theorem comp_dualTensorHom (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) :
    dualTensorHom R N P (g ⊗ₜ[R] p) ∘ₗ dualTensorHom R M N (f ⊗ₜ[R] n) =
      g n • dualTensorHom R M P (f ⊗ₜ p)

Proof state:
case h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ f m • g n • p = g n • f m • p

Tactic:
rw [smul_comm]

Result:
no goals

Proof state:
case h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ((dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n)) m =
    (g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)) m

Tactic:
simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smul,
  RingHom.id_apply, LinearMap.smul_apply]

Result:
case h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ f m • g n • p = g n • f m • p

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
⊢ (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)

Tactic:
ext m

Result:
case h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ((dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n)) m =
    (g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)) m
-- Mathlib/Order/Filter/AtTopBot/Monoid.lean
theorem Tendsto.atTop_of_mul_isBoundedUnder_le (hg : IsBoundedUnder (· ≤ ·) l g)
    (h : Tendsto (fun x => f x * g x) l atTop) : Tendsto f l atTop

Proof state:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 => x1 ≤ x2) x C
⊢ Tendsto f l atTop

Tactic:
refine .atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h

Result:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 => x1 ≤ x2) x C
⊢ (fun x => f x * g x) ≤ᶠ[l] fun x => f x * C

Proof state:
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
hg : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l g
h : Tendsto (fun x => f x * g x) l atTop
⊢ Tendsto f l atTop

Tactic:
obtain ⟨C, hC⟩ := hg

Result:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 => x1 ≤ x2) x C
⊢ Tendsto f l atTop
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_emod_right (a b : Int) : -(a * b) % a = 0

Proof state:
a b : Int
⊢ -(a * b) % a = 0

Tactic:
rw [← dvd_iff_emod_eq_zero, Int.dvd_neg]

Result:
a b : Int
⊢ a ∣ a * b

Proof state:
a b : Int
⊢ a ∣ a * b

Tactic:
exact Int.dvd_mul_right a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} {h₁} :
    (m.insertIfNew k v).get a h₁ =
      if h₂ : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1)) v
      else m.get a (mem_of_mem_insertIfNew' h h₁ h₂)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get a ⋯

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯

Tactic:
simp_to_raw using Raw₀.get_insertIfNew ⟨m, _⟩

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Binomial.lean
@[simp]
lemma binomialSeries_add [Semiring A] [Algebra R A] (r s : R) :
    binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
⊢ binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s

Tactic:
ext n

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
⊢ (coeff A n) (binomialSeries A (r + s)) = (coeff A n) (binomialSeries A r * binomialSeries A s)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
⊢ (coeff A n) (binomialSeries A (r + s)) = (coeff A n) (binomialSeries A r * binomialSeries A s)

Tactic:
simp only [binomialSeries_coeff, Ring.add_choose_eq n (Commute.all r s), coeff_mul,
  Algebra.mul_smul_comm, mul_one, sum_smul]

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
⊢ ∑ i ∈ antidiagonal n, (Ring.choose r i.1 * Ring.choose s i.2) • 1 =
    ∑ x ∈ antidiagonal n, Ring.choose s x.2 • Ring.choose r x.1 • 1

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ (Ring.choose r ab.1 * Ring.choose s ab.2) • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1

Tactic:
rw [mul_comm, mul_smul]

Result:
no goals

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
⊢ ∑ i ∈ antidiagonal n, (Ring.choose r i.1 * Ring.choose s i.2) • 1 =
    ∑ x ∈ antidiagonal n, Ring.choose s x.2 • Ring.choose r x.1 • 1

Tactic:
refine sum_congr rfl fun ab hab => ?_

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ (Ring.choose r ab.1 * Ring.choose s ab.2) • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin_apply (M : Matrix n n R₁) (x y : M₁) :
    Matrix.toBilin b M x y = ∑ i, ∑ j, b.repr x i * M i j * b.repr y j :=
  (Matrix.toLinearMap₂_apply _ _ _ _ _).trans
    (by simp only [smul_eq_mul, mul_assoc, mul_comm, mul_left_comm])

Proof state:
R₁ : Type u_1
M₁ : Type u_2
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Basis n R₁ M₁
M : Matrix n n R₁
x y : M₁
⊢ ∑ i : n, ∑ j : n, (b.repr x) i • (b.repr y) j • M i j = ∑ i : n, ∑ j : n, (b.repr x) i * M i j * (b.repr y) j

Tactic:
simp only [smul_eq_mul, mul_assoc, mul_comm, mul_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_hom_app_zero : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.zero = iX.hom

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem eq_bot_iff : K = ⊥ ↔ ∀ x : L, x ∈ K → x = 0

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
rw [_root_.eq_bot_iff]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0
-- Mathlib/Data/Set/Finite/Basic.lean
theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.Infinite)
    (h_fin : (f '' s).Finite) : ¬InjOn f s

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s

Tactic:
have h := not_injective_infinite_finite
          ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)

Result:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (s.restrict f) (f '' s) ⋯)
⊢ ¬InjOn f s

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (s.restrict f) (f '' s) ⋯)

Tactic:
rwa [injective_codRestrict, ← injOn_iff_injective]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (s.restrict f) (f '' s) ⋯)
⊢ ¬InjOn f s

Tactic:
contrapose! h

Result:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (s.restrict f) (f '' s) ⋯)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
⊢ ¬InjOn f s

Tactic:
have : Finite (f '' s) := finite_coe_iff.mpr h_fin

Result:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite ↑(f '' s)
⊢ ¬InjOn f s

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite ↑(f '' s)
⊢ ¬InjOn f s

Tactic:
have : Infinite s := infinite_coe_iff.mpr h_inf

Result:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_div'' (hab : a < b) (hcd : c < d) : a / d < b / c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
exact mul_lt_mul_of_lt_of_lt hab hcd

Result:
no goals

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]

Result:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_of_subsingleton [Subsingleton R] : natDegree p = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ p.natDegree = 0

Tactic:
rw [Subsingleton.elim p 0, natDegree_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
    zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
⊢ as.toArray.zipWithAux bs.toArray f 0 cs = cs ++ (zipWith f as bs).toArray

Tactic:
rw [Array.zipWithAux]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
⊢ (if h : 0 < as.toArray.size then
      let a := as.toArray[0];
      if h : 0 < bs.toArray.size then
        let b := bs.toArray[0];
        as.toArray.zipWithAux bs.toArray f (0 + 1) (cs.push (f a b))
      else cs
    else cs) =
    cs ++ (zipWith f as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
x✝ : List α
⊢ (if h : 0 < x✝.toArray.size then
      let a := x✝.toArray[0];
      if h : 0 < #[].size then
        let b := #[][0];
        x✝.toArray.zipWithAux #[] f (0 + 1) (cs.push (f a b))
      else cs
    else cs) =
    cs ++ (zipWith f x✝ []).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
x✝ : List β
⊢ (if h : 0 < #[].size then
      let a := #[][0];
      if h : 0 < x✝.toArray.size then
        let b := x✝.toArray[0];
        #[].zipWithAux x✝.toArray f (0 + 1) (cs.push (f a b))
      else cs
    else cs) =
    cs ++ (zipWith f [] x✝).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as✝ : List α
bs✝ : List β
cs : Array γ
a : α
as : List α
b : β
bs : List β
⊢ (if h : 0 < (a :: as).toArray.size then
      let a_1 := (a :: as).toArray[0];
      if h : 0 < (b :: bs).toArray.size then
        let b_1 := (b :: bs).toArray[0];
        (a :: as).toArray.zipWithAux (b :: bs).toArray f (0 + 1) (cs.push (f a_1 b_1))
      else cs
    else cs) =
    cs ++ (zipWith f (a :: as) (b :: bs)).toArray

Tactic:
simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
⊢ (if h : 0 < as.toArray.size then
      let a := as.toArray[0];
      if h : 0 < bs.toArray.size then
        let b := bs.toArray[0];
        as.toArray.zipWithAux bs.toArray f (0 + 1) (cs.push (f a b))
      else cs
    else cs) =
    cs ++ (zipWith f as bs).toArray

Tactic:
match as, bs with
| [], _ => simp
| _, [] => simp
| a :: as, b :: bs =>
  simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (insertMany empty l).1.1.size = l.length

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ empty.val.size + l.length = l.length

Tactic:
simp only [size_empty, Nat.zero_add]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (empty.insertMany l).val.val.size = l.length

Tactic:
rw [size_insertMany_list _ Raw.WF.empty₀ distinct]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ empty.val.size + l.length = l.length

α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ ∀ (a : α), empty.contains a = true → (List.map Sigma.fst l).contains a = false

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ ∀ (a : α), empty.contains a = true → (List.map Sigma.fst l).contains a = false

Tactic:
simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true]

Result:
no goals