harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_append_iff {l : List α} :
    l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂

Proof state:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r :: r₁ ++ r₂
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Tactic:
simp only [cons_append] at w

Result:
case cons.mp
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l : List α
w : l <+ r :: (r₁ ++ r₂)
⊢ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r :: r₁ ∧ l₂ <+ r₂

Proof state:
case cons.mpr.intro.intro.intro.intro.cons₂
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₂ : List α
w₂ : l₂ <+ r₂
l : List α
w₁ : l <+ r₁
⊢ r :: l ++ l₂ <+ r :: r₁ ++ r₂

Tactic:
exact Sublist.cons₂ _ (Sublist.append w₁ w₂)

Result:
no goals

Proof state:
case cons.mpr.intro.intro.intro.intro.cons
α : Type u_1
r₂ : List α
r : α
r₁ : List α
ih : ∀ {l : List α}, l <+ r₁ ++ r₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <+ r₁ ∧ l₂ <+ r₂
l₁ l₂ : List α
w₂ : l₂ <+ r₂
w₁ : l₁ <+ r₁
⊢ l₁ ++ l₂ <+ r :: r₁ ++ r₂

Tactic:
exact Sublist.cons _ (Sublist.append w₁ w₂)

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem erase_mem_compression_of_mem_compression : s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜
⊢ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [erase_eq_of_not_mem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 →
    s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜
⊢ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem neg_of_mem_negA_plusPart (hx : x ∈ negAt s '' (plusPart A)) {w : {w // IsReal w}}
    (hw : w ∈ s) : x.1 w < 0

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hx : x ∈ ⇑(negAt s) '' plusPart A
w : { w // w.IsReal }
hw : w ∈ s
⊢ x.1 w < 0

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ ((negAt s) y).1 w < 0

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ ((negAt s) y).1 w < 0

Tactic:
rw [negAt_apply_isReal_and_mem _ hw, neg_lt_zero]

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Result:
no goals
-- Mathlib/Data/Quot.lean
theorem Quotient.eq_mk_iff_out {s : Setoid α} {x : Quotient s} {y : α} :
    x = ⟦y⟧ ↔ Quotient.out x ≈ y

Proof state:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧

Tactic:
rw [Quotient.out_eq x]

Result:
no goals

Proof state:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x.out ≈ y

Tactic:
refine Iff.trans ?_ Quotient.eq

Result:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem toMatrix_vecMul_coords (x : P) : b₂.coords x ᵥ* b.toMatrix b₂ = b.coords x

Proof state:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = b.coords x j

Tactic:
change _ = b.coord j x

Result:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) x

Proof state:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) x

Tactic:
conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]

Result:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) ((Finset.affineCombination k Finset.univ ⇑b₂) fun i => (b₂.coord i) x)

Proof state:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j =
    (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ ⇑b₂)) fun i => (b₂.coord i) x

Tactic:
simp [Matrix.vecMul, dotProduct, toMatrix_apply, coords]

Result:
no goals

Proof state:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = (b.coord j) ((Finset.affineCombination k Finset.univ ⇑b₂) fun i => (b₂.coord i) x)

Tactic:
rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]

Result:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j =
    (Finset.affineCombination k Finset.univ (⇑(b.coord j) ∘ ⇑b₂)) fun i => (b₂.coord i) x

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
⊢ b₂.coords x ᵥ* b.toMatrix ⇑b₂ = b.coords x

Tactic:
ext j

Result:
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ (b₂.coords x ᵥ* b.toMatrix ⇑b₂) j = b.coords x j
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem not_exists_int_prime_dvd_sub_of_prime_ne_two'
    [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) (hodd : p ≠ 2) :
    ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K))

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ ¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ ¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa using hcycl

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ ¬∃ n, ↑↑p ∣ hζ✝.toInteger - ↑n

Tactic:
exact not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ ¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ ¬∃ n, ↑↑p ∣ hζ✝.toInteger - ↑n
-- Mathlib/LinearAlgebra/Orientation.lean
theorem eq_or_eq_neg_of_isEmpty [IsEmpty ι] (o : Orientation R M ι) :
    o = positiveOrientation ∨ o = -positiveOrientation

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]

Tactic:
intro h

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
⊢ False

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)

Tactic:
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ False

Tactic:
have H : LinearIndependent R ![f x, 1] := by
  convert h.map' f.toLinearMap f.ker
  ext i
  fin_cases i <;> simp [f]

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H : LinearIndependent R ![f x, 1]
⊢ False
-- Mathlib/Topology/Sets/Opens.lean
theorem isOpenEmbedding_of_le {U V : Opens α} (i : U ≤ V) :
    IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i) where
  toIsEmbedding := .inclusion i
  isOpen_range

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}

Tactic:
exact U.isOpen.preimage continuous_subtype_val

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen (range (Set.inclusion ⋯))

Tactic:
rw [Set.range_inclusion i]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen {x | ↑x ∈ ↑U}
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem Prime.not_dvd_finset_prod {S : Finset α} {p : M} (pp : Prime p) {g : α → M}
    (hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoidWithZero M
S : Finset α
p : M
pp : Prime p
g : α → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
exact mt (Prime.dvd_finset_prod_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

Result:
no goals
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem card_le_of_surjective [RankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α → R) →ₗ[R] β → R) (i : Surjective f) : Fintype.card β ≤ Fintype.card α

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card β ≤ Fintype.card α

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card β ≤ Fintype.card α

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
exact
  le_of_fin_surjective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
    (((LinearEquiv.symm Q).surjective.comp i).comp (LinearEquiv.surjective P))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_snd : (unzip l).snd = l.map Prod.snd

Proof state:
α✝ : Type u_1
β✝ : Type u_2
l : Array (α✝ × β✝)
⊢ l.unzip.snd = map Prod.snd l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem hausdorffDist_optimal_le_HD {f} (h : f ∈ candidatesB X Y) :
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD f

Proof state:
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
h : f ∈ GromovHausdorff.candidatesB X Y
r : ℝ
hr : HD (GromovHausdorff.optimalGHDist X Y) < r
z : X
I1 : ⨆ x, ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl x, inr y) < r
I2 :
  ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl z, inr y) ≤ ⨆ x, ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl x, inr y)
I : ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl z, inr y) < r
⊢ ∃ y ∈ range (optimalGHInjr X Y), dist (optimalGHInjl X Y z) y ≤ r

Tactic:
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
h : f ∈ GromovHausdorff.candidatesB X Y
r : ℝ
hr : HD (GromovHausdorff.optimalGHDist X Y) < r
z : X
I1 : ⨆ x, ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl x, inr y) < r
I2 :
  ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl z, inr y) ≤ ⨆ x, ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl x, inr y)
I : ⨅ y, (GromovHausdorff.optimalGHDist X Y) (inl z, inr y) < r
z' : Y
hr' : (fun y => (GromovHausdorff.optimalGHDist X Y) (inl z, inr y)) z' < r
⊢ ∃ y ∈ range (optimalGHInjr X Y), dist (optimalGHInjl X Y z) y ≤ r
-- Mathlib/Control/Traversable/Lemmas.lean
theorem naturality' (η : ApplicativeTransformation F G) (x : t (F α)) :
    η (sequence x) = sequence (@η _ <$> x)

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
η : ApplicativeTransformation F G
x : t (F α)
⊢ (fun {α} => η.app α) (sequence x) = sequence ((fun {α} => η.app α) <$> x)

Tactic:
simp [sequence, naturality, traverse_map]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
theorem inv_right₀ (h : SemiconjBy a x y) : SemiconjBy a x⁻¹ y⁻¹

Proof state:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹

Tactic:
simp [h.resolve_right ha]

Result:
no goals

Proof state:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
have := mul_ne_zero ha hx

Result:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases ha : a = 0

Result:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Proof state:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

Result:
no goals

Proof state:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
simp only [ha, zero_left]

Result:
no goals

Proof state:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
rw [h.eq, mul_ne_zero_iff] at this

Result:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Proof state:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
subst x

Result:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹

Proof state:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases hx : x = 0

Result:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Proof state:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹

Tactic:
simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h

Result:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹
-- Mathlib/Data/Real/Irrational.lean
theorem of_pow : ∀ n : ℕ, Irrational (x ^ n) → Irrational x
  | 0 => fun h => by
    rw [pow_zero] at h
    exact (h ⟨1, cast_one⟩).elim
  | n + 1 => fun h => by
    rw [pow_succ] at h
    exact h.mul_cases.elim (of_pow n) id

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))
⊢ Irrational x

Tactic:
rw [pow_succ] at h

Result:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x

Proof state:
x : ℝ
h : Irrational (x ^ 0)
⊢ Irrational x

Tactic:
rw [pow_zero] at h

Result:
x : ℝ
h : Irrational 1
⊢ Irrational x

Proof state:
x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x

Tactic:
exact h.mul_cases.elim (of_pow n) id

Result:
no goals

Proof state:
x : ℝ
h : Irrational 1
⊢ Irrational x

Tactic:
exact (h ⟨1, cast_one⟩).elim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem self_eq_add_left  {a b : Nat} : a = b + a ↔ b = 0

Proof state:
a b : Nat
⊢ a = b + a ↔ b = 0

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_nonneg_of_forall_setIntegral_nonneg (hf : Integrable f μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
h_int_gt : ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal
⊢ μ {x | f x ≤ b} = 0

Tactic:
contrapose! h_int_gt with H

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ b * (μ s).toReal < ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
⊢ μ {x | f x ≤ b} = 0

Tactic:
let s := {x | f x ≤ b}

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
⊢ μ {x | f x ≤ b} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ b * (μ s).toReal < ∫ (x : α) in s, f x ∂μ

Tactic:
calc
  b * (μ s).toReal < 0 := mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne
  _ ≤ ∫ x in s, f x ∂μ := by
    rw [← μ.restrict_toMeasurable mus.ne]
    exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x

Tactic:
rw [ae_const_le_iff_forall_lt_measure_zero]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ b < 0, μ {x | f x ≤ b} = 0