harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ zipIdx l k) :
    x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)

Proof state:
α : Type u_1
x : α × Nat
k : Nat
toList✝ : List α
h : x ∈ { toList := toList✝ }.zipIdx k
⊢ x ∈ { toList := toList✝ }.toList.zipIdx k

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
x : α × Nat
k : Nat
toList✝ : List α
h : x ∈ { toList := toList✝ }.zipIdx k
⊢ x.fst = { toList := toList✝ }[x.snd - k]

Tactic:
exact List.fst_eq_of_mem_zipIdx (by simpa using h)

Result:
no goals

Proof state:
α : Type ?u.28502
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + l.size
⊢ x.snd - k < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.28502
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < l.size

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.28502
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + l.size
⊢ x.snd - k < l.size

Proof state:
α : Type ?u.28502
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd - k < l.size

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.28502
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < l.size

Proof state:
α : Type u_1
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.fst = l[x.snd - k]

Tactic:
cases l

Result:
case mk
α : Type u_1
x : α × Nat
k : Nat
toList✝ : List α
h : x ∈ { toList := toList✝ }.zipIdx k
⊢ x.fst = { toList := toList✝ }[x.snd - k]
-- Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
theorem effectiveEpi_tfae
    {B X : CompHaus.{u}} (π : X ⟶ B) :
    TFAE
    [ EffectiveEpi π
    , Epi π
    , Function.Surjective π
    ]

Proof state:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Result:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩

Result:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
B X : CompHaus
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance

Result:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
-- Mathlib/Algebra/Group/Commute/Defs.lean
@[to_additive] lemma mul_pow (h : Commute a b) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
  | n + 1 => by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Proof state:
M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_mul_inner_self_le (x y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ :=
  calc
    ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖

Tactic:
exact le_abs_self _

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖

Tactic:
rw [real_inner_comm y, ← norm_mul]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖
-- Mathlib/Algebra/Quandle.lean
theorem assoc_iff_id {R : Type*} [Rack R] {x y z : R} : x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Proof state:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [left_cancel]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [self_distrib]

Result:
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
-- Mathlib/Algebra/Colimit/Module.lean
theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f) :
    ∃ i x, of R ι G f i x = z :=
  Nonempty.elim (by infer_instance) fun ind : ι ↦
    Quotient.inductionOn' z fun z ↦
      DirectSum.induction_on z ⟨ind, 0, LinearMap.map_zero _⟩ (fun i x ↦ ⟨i, x, rfl⟩)
        fun p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩ ↦
        let ⟨k, hik, hjk⟩ := exists_ge_ge i j
        ⟨k, f i k hik x + f j k hjk y, by
          rw [LinearMap.map_add, of_f, of_f, ihx, ihy]
          rfl ⟩

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z : DirectLimit G f
⊢ Nonempty ι

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i => G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x + (f j k hjk) y) = Quotient.mk'' (p + q)

Tactic:
rw [LinearMap.map_add, of_f, of_f, ihx, ihy]

Result:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i => G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i => G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
/-- See also `RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent`. -/
lemma coxeterWeight_eq_four_iff_not_linearIndependent :
    P.coxeterWeight i j = 4 ↔ ¬ LinearIndependent R ![P.root i, P.root j]

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
⊢ P.coxeterWeight i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j]

Tactic:
rw [P.linearIndependent_iff_coxeterWeight_ne_four, not_not]

Result:
no goals
-- Mathlib/CategoryTheory/Presentable/Basic.lean
lemma isCardinalAccessible_of_le
    [F.IsCardinalAccessible κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') :
    F.IsCardinalAccessible κ' where
  preservesColimitOfShape {J _ _}

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
exact F.preservesColimitsOfShape_of_isCardinalAccessible κ J

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
⊢ PreservesColimitsOfShape J F

Tactic:
have := IsCardinalFiltered.of_le J h

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem X_dvd_iff {s : σ} {φ : MvPowerSeries σ R} :
    (X s : MvPowerSeries σ R) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff R m φ = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0

Tactic:
rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff R m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff R m) φ = 0
m : σ →₀ ℕ
hm : m s = 0
⊢ (coeff R m) φ = 0

Tactic:
exact h m (hm.symm ▸ zero_lt_one)

Result:
no goals

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff R m) φ = 0

Tactic:
exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm)

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff R m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0

Tactic:
constructor <;> intro h m hm

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff R m) φ = 0
m : σ →₀ ℕ
hm : m s = 0
⊢ (coeff R m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff R m) φ = 0
-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_smul (g : HNNExtension G A B φ) (w : NormalWord d) :
    (g • w).prod φ = g * w.prod φ

Proof state:
case t
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ ReducedWord.prod φ (t • w).toReducedWord = t * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [t_smul_eq_unitsSMul, prod_unitsSMul, mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : HNNExtension G A B φ
w : NormalWord d
⊢ ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord

Tactic:
induction g using induction_on generalizing w with
| of => simp [of_smul_eq_smul]
| t => simp [t_smul_eq_unitsSMul, prod_unitsSMul, mul_assoc]
| mul => simp_all [mul_smul, mul_assoc]
| inv x ih =>
  rw [← mul_right_inj x, ← ih]
  simp

Result:
no goals

Proof state:
case mul
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x✝ y✝ : HNNExtension G A B φ
a✝¹ : ∀ (w : NormalWord d), ReducedWord.prod φ (x✝ • w).toReducedWord = x✝ * ReducedWord.prod φ w.toReducedWord
a✝ : ∀ (w : NormalWord d), ReducedWord.prod φ (y✝ • w).toReducedWord = y✝ * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ ((x✝ * y✝) • w).toReducedWord = x✝ * y✝ * ReducedWord.prod φ w.toReducedWord

Tactic:
simp_all [mul_smul, mul_assoc]

Result:
no goals

Proof state:
case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x⁻¹ • w).toReducedWord = x⁻¹ * ReducedWord.prod φ w.toReducedWord

Tactic:
rw [← mul_right_inj x, ← ih]

Result:
case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)

Proof state:
case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp

Result:
no goals

Proof state:
case of
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w : NormalWord d
⊢ ReducedWord.prod φ (of g✝ • w).toReducedWord = of g✝ * ReducedWord.prod φ w.toReducedWord

Tactic:
simp [of_smul_eq_smul]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.sup' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    (l ⊔ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2 :=
  ⟨by
    intro t
    simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]
    simp only [and_assoc, and_left_comm]⟩

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t

Tactic:
simp only [and_assoc, and_left_comm]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
   ← exists_and_right, ← exists_and_left]

Result:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ∀ (t : Set α), t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
intro t

Result:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t
-- Mathlib/Order/SuccPred/Basic.lean
@[simp, norm_cast]
lemma coe_pred_of_mem [PredOrder α] {a : s} (h : pred a.1 ∈ s) :
    (pred a).1 = pred ↑a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(pred a) = pred ↑a

Tactic:
classical
change Subtype.val (dite ..) = _
simp [h]

Result:
no goals

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(pred a) = pred ↑a

Tactic:
change Subtype.val (dite ..) = _

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(if h : pred ↑a ∈ s then ⟨pred ↑a, h⟩ else a) = pred ↑a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(if h : pred ↑a ∈ s then ⟨pred ↑a, h⟩ else a) = pred ↑a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem ofOption_dom {α} : ∀ o : Option α, (ofOption o).Dom ↔ o.isSome
  | Option.none => by simp [ofOption, none]
  | Option.some a => by simp [ofOption]

Proof state:
α : Type u_4
⊢ (↑Option.none).Dom ↔ Option.none.isSome = true

Tactic:
simp [ofOption, none]

Result:
no goals

Proof state:
α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ (Option.some a).isSome = true

Tactic:
simp [ofOption]

Result:
no goals
-- Mathlib/NumberTheory/KummerDedekind.lean
theorem prod_mem_ideal_map_of_mem_conductor {p : R} {z : S}
    (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)) (hz' : z ∈ I.map (algebraMap R S)) :
    algebraMap R S p * z ∈ algebraMap R<x> S '' ↑(I.map (algebraMap R R<x>))

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
    (algebraMap R S) a * ((algebraMap R S) p * l a)

Tactic:
simp only [RingHom.map_mul, mul_comm (algebraMap R S p) (l a)]

Result:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a) *
      (algebraMap (↥(adjoin R {x})) S) ⟨l a * (algebraMap R S) p, ⋯⟩ =
    (algebraMap R S) a * (l a * (algebraMap R S) p)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma MutuallySingular.rnDeriv_ae_eq_zero (hμν : μ ⟂ₘ ν) :
    μ.rnDeriv ν =ᵐ[ν] 0

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ ⟂ₘ ν

Tactic:
exact hμν

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ ⟂ₘ ν

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

Tactic:
by_cases h : μ.HaveLebesgueDecomposition ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0
-- Mathlib/Data/Finset/NAry.lean
theorem card_le_card_image₂_left {s : Finset α} (hs : s.Nonempty) (hf : ∀ a, Injective (f a)) :
    #t ≤ #(image₂ f s t)

Proof state:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ #(image₂ f {a} t) ≤ #(image₂ f s t)

Tactic:
exact card_le_card (image₂_subset_right <| singleton_subset_iff.2 ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
s : Finset α
hs : s.Nonempty
hf : ∀ (a : α), Injective (f a)
⊢ #t ≤ #(image₂ f s t)

Tactic:
obtain ⟨a, ha⟩ := hs

Result:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ #t ≤ #(image₂ f s t)

Proof state:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ #t ≤ #(image₂ f s t)

Tactic:
rw [← card_image₂_singleton_left _ (hf a)]

Result:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
s : Finset α
hf : ∀ (a : α), Injective (f a)
a : α
ha : a ∈ s
⊢ #(image₂ f {a} t) ≤ #(image₂ f s t)
-- Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
theorem ι_colimitCompWhiskeringRightIsoColimitComp_hom {C : Type*} [Category C] {D : Type*}
    [Category D] {E : Type*} [Category E] {J : Type*} [Category J]
    [HasColimitsOfShape J D] (F : D ⥤ E) [PreservesColimitsOfShape J F] (G : J ⥤ C ⥤ D) (j : J) :
    colimit.ι (G ⋙ (whiskeringRight _ _ _).obj F) j ≫
      (colimitCompWhiskeringRightIsoColimitComp F G).hom = whiskerRight (colimit.ι G j) F

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{u_7, u_3} E
J : Type u_4
inst✝² : Category.{u_8, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom =
    whiskerRight (colimit.ι G j) F

Tactic:
simp [colimitCompWhiskeringRightIsoColimitComp]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem inverse_counitInv_comp (e : C ≌ D) (Y : D) :
    e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)

Tactic:
erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y))
    (Iso.refl _)]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)).hom =
    (Iso.refl ((𝟭 C).obj (e.inverse.obj Y))).hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)).hom =
    (Iso.refl ((𝟭 C).obj (e.inverse.obj Y))).hom

Tactic:
exact e.unit_inverse_comp Y

Result:
no goals