harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_bot_le_iff {i n : ι} {ω : Ω} (hx : ∃ j, j ≤ n ∧ u j ω ∈ s) :
    hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Proof state:
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
simp only [(hitting_le ω).trans hi, true_iff]

Result:
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
⊢ ∃ j ≤ i, u j ω ∈ s

Proof state:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
rw [hitting_le_iff_of_lt _ hi]

Result:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
⊢ (∃ j ∈ Set.Icc ⊥ i, u j ω ∈ s) ↔ ∃ j ≤ i, u j ω ∈ s

Proof state:
case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
⊢ ∃ j ≤ i, u j ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hx

Result:
case inr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hi : n ≤ i
j : ι
hj₁ : j ≤ n
hj₂ : u j ω ∈ s
⊢ ∃ j ≤ i, u j ω ∈ s

Proof state:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
⊢ (∃ j ∈ Set.Icc ⊥ i, u j ω ∈ s) ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hi : n ≤ i
j : ι
hj₁ : j ≤ n
hj₂ : u j ω ∈ s
⊢ ∃ j ≤ i, u j ω ∈ s

Tactic:
exact ⟨j, hj₁.trans hi, hj₂⟩

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
rcases lt_or_le i n with hi | hi

Result:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrderBot ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
⊢ hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
-- Mathlib/Computability/TuringMachine.lean
theorem tr_eval (k) (L : List (Γ k)) {L₁ L₂} (H₁ : L₁ ∈ TM1.eval (tr M) (trInit k L))
    (H₂ : L₂ ∈ TM2.eval M k L) :
    ∃ (S : ∀ k, List (Γ k)) (L' : ListBlank (∀ k, Option (Γ k))),
      addBottom L' = L₁ ∧
        (∀ k, L'.map (proj k) = ListBlank.mk ((S k).map some).reverse) ∧ S k = L₂

Proof state:
case intro.intro.intro.intro
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))
H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)
c₂ : TM2.Cfg Γ Λ σ
h₂ : c₂ ∈ eval (TM2.step M) (TM2.init k L)
H₂ : c₂.stk k ∈ TM2.eval M k L
⊢ ∃ S L',
    addBottom L' = c₁.Tape.right₀ ∧
      (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧ S k = c₂.stk k

Tactic:
obtain ⟨_, ⟨L', hT⟩, h₃⟩ := Turing.tr_eval (tr_respects M) (trCfg_init k L) h₂

Result:
case intro.intro.intro.intro.intro.intro.mk
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
c₁ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
h₁ : c₁ ∈ eval (TM1.step (tr M)) (TM1.init (trInit k L))
H₁ : c₁.Tape.right₀ ∈ TM1.eval (tr M) (trInit k L)
q✝ : Option Λ
v✝ : σ
S✝ : (k : K) → List (Γ k)
L' : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S✝ k)).reverse
h₂ : { l := q✝, var := v✝, stk := S✝ } ∈ eval (TM2.step M) (TM2.init k L)
H₂ : { l := q✝, var := v✝, stk := S✝ }.stk k ∈ TM2.eval M k L
h₃ :
  { l := Option.map normal q✝, var := v✝, Tape := Tape.mk' ∅ (addBottom L') } ∈
    eval (TM1.step (tr M)) (TM1.init (trInit k L))
⊢ ∃ S L',
    addBottom L' = c₁.Tape.right₀ ∧
      (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S k)).reverse) ∧
        S k = { l := q✝, var := v✝, stk := S✝ }.stk k
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.orthonormal_of_forall_eq_or_eq_neg {v w : ι → E} (hv : Orthonormal 𝕜 v)
    (hw : ∀ i, w i = v i ∨ w i = -v i) : Orthonormal 𝕜 w

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ ∀ (i j : ι), inner (w i) (w j) = if i = j then 1 else 0

Tactic:
intro i j

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
⊢ inner (w i) (w j) = if i = j then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
⊢ inner (w i) (w j) = if i = j then 1 else 0

Tactic:
rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
  replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
  simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
    neg_eq_zero] using hv

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ Orthonormal 𝕜 w

Tactic:
rw [orthonormal_iff_ite] at *

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ ∀ (i j : ι), inner (w i) (w j) = if i = j then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ Orthonormal 𝕜 w

Tactic:
classical
rw [orthonormal_iff_ite] at *
intro i j
rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
  replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
  simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
    neg_eq_zero] using hv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
  | 0, _, _ => by simp
  | _, 0, _ => by simp
  | _, _, [] => by simp
  | m+1, n+1, h :: t => by
    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
    congr 1
    omega

Proof state:
α : Type u_1
m n : Nat
h : α
t : List α
⊢ min (m - n) (t.length - n) = min (m + 1 - (n + 1)) (t.length - n)

Tactic:
congr 1

Result:
case e_a
α : Type u_1
m n : Nat
h : α
t : List α
⊢ m - n = m + 1 - (n + 1)

Proof state:
α : Type u_1
x✝¹ x✝ : Nat
⊢ drop x✝ (take x✝¹ []) = take (x✝¹ - x✝) (drop x✝ [])

Tactic:
simp

Result:
no goals

Proof state:
case e_a
α : Type u_1
m n : Nat
h : α
t : List α
⊢ m - n = m + 1 - (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
h : α
t : List α
⊢ drop (n + 1) (take (m + 1) (h :: t)) = take (m + 1 - (n + 1)) (drop (n + 1) (h :: t))

Tactic:
simp [take_succ_cons, drop_succ_cons, drop_take m n t]

Result:
α : Type u_1
m n : Nat
h : α
t : List α
⊢ min (m - n) (t.length - n) = min (m + 1 - (n + 1)) (t.length - n)

Proof state:
α : Type u_1
x✝¹ : Nat
x✝ : List α
⊢ drop x✝¹ (take 0 x✝) = take (0 - x✝¹) (drop x✝¹ x✝)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x✝¹ : Nat
x✝ : List α
⊢ drop 0 (take x✝¹ x✝) = take (x✝¹ - 0) (drop 0 x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/--
**Hadamard three-line theorem** on `re ⁻¹' [0, 1]`: If `f` is a bounded function, continuous on the
closed strip `re ⁻¹' [0, 1]` and differentiable on open strip `re ⁻¹' (0, 1)`, then for
`M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x}))` we have that for all `z` in the closed strip
`re ⁻¹' [0, 1]` the inequality `‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re` holds. -/
lemma norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ (f : ℂ → E) {z : ℂ}
    (hz : z ∈ verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) :
    ‖f z‖ ≤ ‖interpStrip f z‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
apply le_on_closure (fun w hw ↦ norm_le_interpStrip_of_mem_verticalStrip_zero f w hd hB hw)
  (Continuous.comp_continuousOn' continuous_norm hd.2)
  (Continuous.comp_continuousOn' continuous_norm (diffContOnCl_interpStrip f).2)

Result:
case hx
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)

Proof state:
case hx
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)

Tactic:
rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.multiplicity_lt_iff_not_dvd {k : ℕ} (hf : FiniteMultiplicity a b) :
    multiplicity a b < k ↔ ¬a ^ k ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬a ^ k ∣ b

Tactic:
rw [hf.pow_dvd_iff_le_multiplicity, not_le]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.fiberwise_left :
    f =Θ[l ×ˢ l'] g → ∀ᶠ y in l', (f ⟨·, y⟩) =Θ[l] (g ⟨·, y⟩)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun x => f (x, y)) =Θ[l] fun x => g (x, y)

Tactic:
simp only [IsTheta, eventually_and]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l', (fun x_1 => f (x_1, x)) =O[l] fun x_1 => g (x_1, x)) ∧
      ∀ᶠ (x : β) in l', (fun x_1 => g (x_1, x)) =O[l] fun x_1 => f (x_1, x)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : β) in l', (fun x_1 => f (x_1, x)) =O[l] fun x_1 => g (x_1, x)) ∧
      ∀ᶠ (x : β) in l', (fun x_1 => g (x_1, x)) =O[l] fun x_1 => f (x_1, x)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem integral_circleTransform (f : ℂ → E) :
    (∫ θ : ℝ in (0)..2 * π, circleTransform R z w f θ) =
      (2 * ↑π * I)⁻¹ • ∮ z in C(z, R), (z - w)⁻¹ • f z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0 ..2 * π, circleTransform R z w f θ = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z

Tactic:
simp_rw [circleTransform, circleIntegral, deriv_circleMap, circleMap]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0 ..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I)) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0 ..2 * π,
        ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0 ..2 * π,
      (2 * ↑π * I)⁻¹ • ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I)) =
    (2 * ↑π * I)⁻¹ •
      ∫ (θ : ℝ) in 0 ..2 * π,
        ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I))

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueSet_one (G : SimpleGraph α) : G.cliqueSet 1 = Set.range singleton :=
  Set.ext fun s => by simp [eq_comm]

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s ∈ G.cliqueSet 1 ↔ s ∈ Set.range singleton

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem min_mul_distrib (a b c : α) : min a (b * c) = min a (min a b * min a c)

Proof state:
case inr.inl
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Tactic:
simp [hc, le_mul_left]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Tactic:
rcases le_total a b with hb | hb

Result:
case inl
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

case inr
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Proof state:
case inr
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Tactic:
rcases le_total a c with hc | hc

Result:
case inr.inl
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

case inr.inr
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Proof state:
case inl
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : a ≤ b
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Tactic:
simp [hb, le_mul_right]

Result:
no goals

Proof state:
case inr.inr
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

Tactic:
simp [hb, hc]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Dense.prod {s : Set X} {t : Set Y} (hs : Dense s) (ht : Dense t) : Dense (s ×ˢ t) :=
  fun x => by
  rw [closure_prod_eq]
  exact ⟨hs x.1, ht x.2⟩

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure (s ×ˢ t)

Tactic:
rw [closure_prod_eq]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure s ×ˢ closure t

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure s ×ˢ closure t

Tactic:
exact ⟨hs x.1, ht x.2⟩

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma isConjExponent_one_div (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
    (1 / a).IsConjExponent (1 / b)

Proof state:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (1 / a).IsConjExponent (1 / b)

Tactic:
simpa using IsConjExponent.inv_inv ha hb hab

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem mem_verts_of_mem_edge {G' : Subgraph G} {e : Sym2 V} {v : V} (he : e ∈ G'.edgeSet)
    (hv : v ∈ e) : v ∈ G'.verts

Proof state:
case h.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ : V
he : s(x✝, v) ∈ G'.edgeSet
hv : v ∈ s(x✝, v)
⊢ v ∈ G'.verts

Tactic:
exact G'.edge_vert (G'.symm he)

Result:
no goals

Proof state:
case h.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v y✝ : V
he : s(v, y✝) ∈ G'.edgeSet
hv : v ∈ s(v, y✝)
⊢ v ∈ G'.verts

Tactic:
exact G'.edge_vert he

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
v : V
he : e ∈ G'.edgeSet
hv : v ∈ e
⊢ v ∈ G'.verts

Tactic:
induction e

Result:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ y✝ : V
he : s(x✝, y✝) ∈ G'.edgeSet
hv : v ∈ s(x✝, y✝)
⊢ v ∈ G'.verts

Proof state:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ y✝ : V
he : s(x✝, y✝) ∈ G'.edgeSet
hv : v ∈ s(x✝, y✝)
⊢ v ∈ G'.verts

Tactic:
rcases Sym2.mem_iff.mp hv with (rfl | rfl)

Result:
case h.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v y✝ : V
he : s(v, y✝) ∈ G'.edgeSet
hv : v ∈ s(v, y✝)
⊢ v ∈ G'.verts

case h.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ : V
he : s(x✝, v) ∈ G'.edgeSet
hv : v ∈ s(x✝, v)
⊢ v ∈ G'.verts
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b

Proof state:
case zero
a : Nat
⊢ ↑(a ^ 0) = ↑a ^ 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
a b : Nat
ih : ↑(a ^ b) = ↑a ^ b
⊢ ↑(a ^ (b + 1)) = ↑a ^ (b + 1)

Tactic:
rw [Nat.pow_succ, Int.ofNat_mul, ih]

Result:
case succ
a b : Nat
ih : ↑(a ^ b) = ↑a ^ b
⊢ ↑a ^ b * ↑a = ↑a ^ (b + 1)

Proof state:
case succ
a b : Nat
ih : ↑(a ^ b) = ↑a ^ b
⊢ ↑a ^ b * ↑a = ↑a ^ (b + 1)

Tactic:
rfl

Result:
no goals

Proof state:
a b : Nat
⊢ ↑(a ^ b) = ↑a ^ b

Tactic:
induction b with
| zero => rfl
| succ b ih => rw [Nat.pow_succ, Int.ofNat_mul, ih]; rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_and {x y : BitVec v} : (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)

Proof state:
v i : Nat
x y : BitVec v
⊢ (x &&& y).toNat.testBit i = (x.toNat.testBit i && y.toNat.testBit i)

Tactic:
simp

Result:
no goals

Proof state:
v i : Nat
x y : BitVec v
⊢ (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)

Tactic:
rw [← testBit_toNat, getLsbD, getLsbD]

Result:
v i : Nat
x y : BitVec v
⊢ (x &&& y).toNat.testBit i = (x.toNat.testBit i && y.toNat.testBit i)
-- Mathlib/Data/Rel.lean
theorem image_inter_dom_eq (s : Set α) : r.image (s ∩ r.dom) = r.image s

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
h : ∃ x_1 ∈ s, r x_1 x
⊢ ∃ x_1 ∈ s ∩ r.dom, r x_1 x

Tactic:
rcases h with ⟨y, hy, ryx⟩

Result:
case a.intro.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ ∃ x_1 ∈ s ∩ r.dom, r x_1 x

Proof state:
case a.intro.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ ∃ x_1 ∈ s ∩ r.dom, r x_1 x

Tactic:
use y

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ y ∈ s ∩ r.dom ∧ r y x

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
h : y ∈ r.dom
⊢ y ∈ s ∩ r.dom ∧ r y x

Tactic:
simp_all only [Set.mem_inter_iff, and_self]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ y ∈ s ∩ r.dom ∧ r y x

Tactic:
suffices h : y ∈ r.dom by simp_all only [Set.mem_inter_iff, and_self]

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ y ∈ r.dom

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ y ∈ r.dom

Tactic:
rw [dom, Set.mem_setOf_eq]

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ ∃ y_1, r y y_1

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.image s ⊆ r.image (s ∩ r.dom)

Tactic:
intro x h

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
h : x ∈ r.image s
⊢ x ∈ r.image (s ∩ r.dom)

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ s ∩ r.dom ≤ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.image (s ∩ r.dom) = r.image s

Tactic:
apply Set.eq_of_subset_of_subset

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.image (s ∩ r.dom) ⊆ r.image s

case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.image s ⊆ r.image (s ∩ r.dom)

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ r.image (s ∩ r.dom) ⊆ r.image s

Tactic:
apply r.image_mono (by simp)

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
h : x ∈ r.image s
⊢ x ∈ r.image (s ∩ r.dom)

Tactic:
rw [mem_image] at *

Result:
case a
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
h : ∃ x_1 ∈ s, r x_1 x
⊢ ∃ x_1 ∈ s ∩ r.dom, r x_1 x

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : β
y : α
hy : y ∈ s
ryx : r y x
⊢ ∃ y_1, r y y_1

Tactic:
use x

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem inv_zero : (0 : R[R⁰⁻¹])⁻¹ = 0

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ (if hr : 0 = 0 then 0 else ↑1 /ₒ ⟨0, ⋯⟩) = 0 /ₒ 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ 0⁻¹ = 0

Tactic:
rw [OreLocalization.zero_def, OreLocalization.inv_def]

Result:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ (if hr : 0 = 0 then 0 else ↑1 /ₒ ⟨0, ⋯⟩) = 0 /ₒ 1