harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/CountableInter.lean
theorem countable_bInter_mem {ι : Type*} {S : Set ι} (hS : S.Countable) {s : ∀ i ∈ S, Set α} :
    (⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l ↔ ∀ i, ∀ hi : i ∈ S, s i ‹_› ∈ l

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
rw [biInter_eq_iInter]

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
haveI := hS.toEncodable

Result:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
s : (i : ι) → i ∈ S → Set α
this : Encodable ↑S
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact countable_iInter_mem.trans Subtype.forall

Result:
no goals
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem ne_bot_of_isMaximal_of_not_isField [Nontrivial R] {M : Ideal R} (max : M.IsMaximal)
    (not_field : ¬IsField R) : M ≠ ⊥

Proof state:
case mk.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
⊢ False

Tactic:
obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field

Result:
case mk.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : M.IsMaximal
not_field : ¬IsField R
⊢ M ≠ ⊥

Tactic:
rintro h

Result:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : M.IsMaximal
not_field : ¬IsField R
h : M = ⊥
⊢ False

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : ⊥.IsMaximal
not_field : ¬IsField R
h : M = ⊥
⊢ False

Tactic:
rcases max with ⟨⟨_h1, h2⟩⟩

Result:
case mk.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
⊢ False

Proof state:
case mk.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False

Tactic:
exact ne_of_lt hItop (h2 I hIbot)

Result:
no goals

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : M.IsMaximal
not_field : ¬IsField R
h : M = ⊥
⊢ False

Tactic:
rw [h] at max

Result:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : ⊥.IsMaximal
not_field : ¬IsField R
h : M = ⊥
⊢ False
-- Mathlib/Data/Multiset/Powerset.lean
theorem revzip_powersetAux {l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux l)) : x.1 + x.2 = ↑l

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h

Result:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a ∈ l.sublists.revzip, Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Proof state:
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l

Tactic:
exact Quot.sound (revzip_sublists _ _ _ h)

Result:
no goals

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a ∈ l.sublists.revzip, Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Result:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Result:
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem exist_unique_vadd_mem_fundamentalDomain [Finite ι] (x : E) :
    ∃! v : span ℤ (Set.range b), v +ᵥ x ∈ fundamentalDomain b

Proof state:
case intro.refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
h : (fun v => v +ᵥ x ∈ fundamentalDomain b) y
⊢ y = -floor b x

Tactic:
exact (vadd_mem_fundamentalDomain b y x).mp h

Result:
no goals

Proof state:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b

Tactic:
refine ⟨-floor b x, ?_, fun y h => ?_⟩

Result:
case intro.refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ (fun v => v +ᵥ x ∈ fundamentalDomain b) (-floor b x)

case intro.refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
h : (fun v => v +ᵥ x ∈ fundamentalDomain b) y
⊢ y = -floor b x

Proof state:
case intro.refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ (fun v => v +ᵥ x ∈ fundamentalDomain b) (-floor b x)

Tactic:
exact (vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b

Tactic:
cases nonempty_fintype ι

Result:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b
-- Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
theorem det_eq_sum_row_mul_submatrix_succAbove_succAbove_det {n : ℕ}
    (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1))
    (hv : ∀ i ≠ i₀, ∑ j, M i j = 0) :
    M.det = (-1) ^ (i₀ + j₀ : ℕ) *
      (∑ j, M i₀ j) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j : Fin (n + 1), M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp_rw [transpose_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j : Fin (n + 1), M i j = 0
⊢ M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ j : Fin (n + 1), M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀
  (by simpa using hv), ← det_transpose, transpose_submatrix, transpose_transpose, add_comm]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j : Fin (n + 1), M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j : Fin (n + 1), M i j = 0
⊢ ∀ (j : Fin (n + 1)), j ≠ i₀ → ∑ i : Fin (n + 1), Mᵀ i j = 0

Tactic:
simpa using hv

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLEMk_comp_ofMkLEMk {B A₁ A₂ : C} (X : Subobject B) (f : A₁ ⟶ B) [Mono f] (g : A₂ ⟶ B)
    [Mono g] (h₁ : X ≤ mk f) (h₂ : mk f ≤ mk g) :
    ofLEMk X f h₁ ≫ ofMkLEMk f g h₂ = ofLEMk X g (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ X.ofLEMk f h₁ ≫ ofMkLEMk f g h₂ = X.ofLEMk g ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying,
  assoc, Iso.hom_inv_id_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom = underlying.map ⋯.hom ≫ (underlyingIso g).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom = underlying.map ⋯.hom ≫ (underlyingIso g).hom

Tactic:
congr 1

Result:
no goals
-- Mathlib/NumberTheory/KummerDedekind.lean
theorem conductor_eq_top_of_adjoin_eq_top (h : R<x> = ⊤) : conductor R x = ⊤

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
h : adjoin R {x} = ⊤
⊢ conductor R x = ⊤

Tactic:
simp only [Ideal.eq_top_iff_one, mem_conductor_iff, h, mem_top, forall_const]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem mul_swap_eq_iff {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j

Proof state:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j = σ ↔ i = j

Tactic:
rw [mul_right_eq_self, swap_eq_one_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem zero_of_padicNorm_eq_zero {q : ℚ} (h : padicNorm p q = 0) : q = 0

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬↑p ^ (-padicValRat p q) = 0

Tactic:
apply zpow_ne_zero

Result:
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ↑p ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ q = 0

Tactic:
apply by_contradiction

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ ¬q = 0 → False

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False

Tactic:
rw [if_neg hq] at h

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ False

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
hq : ¬q = 0
⊢ False

Tactic:
unfold padicNorm at h

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False

Proof state:
case a.a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp.1.ne_zero

Result:
no goals

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ ¬q = 0 → False

Tactic:
intro hq

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
hq : ¬q = 0
⊢ False

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ False

Tactic:
apply absurd h

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬↑p ^ (-padicValRat p q) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_eq_of_size_le {l : Vector α n} {m : Nat} (h : l.size ≤ m) {a : α} :
    l.setIfInBounds m a = l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m : Nat
h : l.size ≤ m
a : α
⊢ l.setIfInBounds m a = l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
a : α
l : Array α
h : { toArray := l, size_toArray := ⋯ }.size ≤ m
⊢ { toArray := l, size_toArray := ⋯ }.setIfInBounds m a = { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
m : Nat
a : α
l : Array α
h : { toArray := l, size_toArray := ⋯ }.size ≤ m
⊢ { toArray := l, size_toArray := ⋯ }.setIfInBounds m a = { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.setIfInBounds_eq_of_size_le (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
m : Nat
a : α
l : Array α
h : { toArray := l, size_toArray := ⋯ }.size ≤ m
⊢ Array.size ?m.163752 ≤ ?m.163753

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_allOnes_lt {x : BitVec w} : ¬allOnes w < x

Proof state:
w : Nat
x : BitVec w
⊢ ¬allOnes w < x

Tactic:
have : 2^w ≠ 0 := Ne.symm (NeZero.ne' (2^w))

Result:
w : Nat
x : BitVec w
this : 2 ^ w ≠ 0
⊢ ¬allOnes w < x

Proof state:
w : Nat
x : BitVec w
this : 2 ^ w ≠ 0
⊢ ¬allOnes w < x

Tactic:
rw [BitVec.not_lt, le_def, Nat.le_iff_lt_add_one, toNat_allOnes, Nat.sub_one_add_one this]

Result:
w : Nat
x : BitVec w
this : 2 ^ w ≠ 0
⊢ x.toNat < 2 ^ w

Proof state:
w : Nat
x : BitVec w
this : 2 ^ w ≠ 0
⊢ x.toNat < 2 ^ w

Tactic:
exact isLt x

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
@[simp] lemma finsuppAntidiag_zero (s : Finset ι) : finsuppAntidiag s (0 : μ) = {0}

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq μ
inst✝² : OrderedAddCommMonoid μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag 0 ↔ f ∈ {0}

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), -mem_piAntidiag, eq_comm]

Result:
no goals

Proof state:
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq μ
inst✝² : OrderedAddCommMonoid μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
⊢ s.finsuppAntidiag 0 = {0}

Tactic:
ext f

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq μ
inst✝² : OrderedAddCommMonoid μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag 0 ↔ f ∈ {0}
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csSup_le_csSup' {s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) : sSup s ≤ sSup t

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

Tactic:
rw [csSup_empty]

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t

Tactic:
exact bot_le

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
exact csSup_le_csSup h₁ h h₂

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | h

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_antitoneOn_Iio :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Iio 0)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
⊢ AntitoneOn (fun x => x⁻¹) (Set.Iio 0)

Tactic:
convert sub_inv_antitoneOn_Iio

Result:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
x✝ : α
⊢ x✝ = x✝ - 0

Proof state:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem coe_derivedSeries_eq_int_aux (R₁ R₂ L : Type*) [CommRing R₁] [CommRing R₂]
    [LieRing L] [LieAlgebra R₁ L] [LieAlgebra R₂ L] (k : ℕ)
    (ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤) :
    let I := derivedSeriesOfIdeal R₂ L k ⊤; let S : Set L := {⁅a, b⁆ | (a ∈ I) (b ∈ I)}
    (Submodule.span R₁ S : Set L) ≤ (Submodule.span R₂ S : Set L)

Proof state:
case smul_mem.intro.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ c • ⁅a, b⁆ ∈ Submodule.span R₂ S

Tactic:
rw [← smul_lie]

Result:
case smul_mem.intro.intro.intro.intro
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ ⁅c • a, b⁆ ∈ Submodule.span R₂ S
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[reassoc]
lemma shift_app (a : A) (X : C) :
    (τ.app X)⟦a⟧' = (F₁.commShiftIso a).inv.app X ≫
      τ.app (X⟦a⟧) ≫ (F₂.commShiftIso a).hom.app X

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_7, u_1} C
inst✝⁶ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ (shiftFunctor D a).map (τ.app X) =
    (F₁.commShiftIso a).inv.app X ≫ τ.app ((shiftFunctor C a).obj X) ≫ (F₂.commShiftIso a).hom.app X

Tactic:
rw [← shift_app_comm, Iso.inv_hom_id_app_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_setToL1 (f : α →₁[μ] E) :
    integral f = setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM f = (setToL1 ⋯) f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = (setToL1 ⋯) f

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM f = (setToL1 ⋯) f
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_map : (p.map f).map f' = p.map (f'.comp f)

Proof state:
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : Walk.map f' (Walk.map f p✝) = Walk.map (f'.comp f) p✝
⊢ Walk.map f' (Walk.map f (cons h✝ p✝)) = Walk.map (f'.comp f) (cons h✝ p✝)

Tactic:
simp [ih]

Result:
no goals

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v : V
p : G.Walk u v
⊢ Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp [ih]

Result:
no goals

Proof state:
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v : V
p : G.Walk u v
u✝ : V
⊢ Walk.map f' (Walk.map f nil) = Walk.map (f'.comp f) nil

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem terminatedAt_iff_partNum_none : g.TerminatedAt n ↔ g.partNums.get? n = none

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partNums.get? n = none

Tactic:
rw [terminatedAt_iff_s_none, partNum_none_iff_s_none]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem findP?_insert_of_ne [@TransCmp α cmp] [IsStrictCut cmp cut]
    (t : RBSet α cmp) (h : cut v ≠ .eq) : (t.insert v).findP? cut = t.findP? cut

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ t.find? v ≠ some u

Tactic:
exact mt (fun h => by rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]) h

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v

Tactic:
rintro rfl

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ (t.insert v).toList ↔ u ∈ t.toList

Tactic:
rw [mem_toList_insert, or_iff_left, and_iff_left]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ t.find? v ≠ some u

α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ ¬u = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h✝ : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
h : t.find? v = some u
⊢ cut v = Ordering.eq

Tactic:
rwa [IsCut.congr (cut := cut) (find?_some_eq_eq h)]

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
⊢ (t.insert v).findP? cut = t.findP? cut

Tactic:
refine Option.ext fun u =>
  findP?_some.trans <| .trans (and_congr_left fun h' => ?_) findP?_some.symm

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
v : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
h : cut v ≠ Ordering.eq
u : α
h' : cut u = Ordering.eq
⊢ u ∈ (t.insert v).toList ↔ u ∈ t.toList

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
u : α
h' : cut u = Ordering.eq
h : cut u ≠ Ordering.eq
⊢ False

Tactic:
contradiction

Result:
no goals