harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_bind (m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} :
    ((bind m) fun a => (bind n) fun b => f a b) = (bind n) fun b => (bind m) fun a => f a b :=
  Multiset.induction_on m (by simp) (by simp +contextual)

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ (bind 0 fun a => n.bind fun b => f a b) = n.bind fun b => bind 0 fun a => f a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a => n.bind fun b => f a b) = n.bind fun b => s.bind fun a => f a b) →
      ((a ::ₘ s).bind fun a => n.bind fun b => f a b) = n.bind fun b => (a ::ₘ s).bind fun a => f a b

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma iSup_basicOpen_eq_top_iff' {s : Set R} :
    (⨆ i ∈ s, PrimeSpectrum.basicOpen i) = ⊤ ↔ Ideal.span s = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤

Tactic:
conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ ⨆ i, basicOpen ↑i = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ ⨆ i, basicOpen ↑i = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_of_length_le {l : List α} (h : l.length ≤ i) : take i l = l

Proof state:
α : Type u_1
i : Nat
l : List α
h : l.length ≤ i
this : take i l = l
⊢ take i l = l

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u_1
i : Nat
l : List α
h : l.length ≤ i
⊢ take i l = l

Tactic:
have := take_append_drop i l

Result:
α : Type u_1
i : Nat
l : List α
h : l.length ≤ i
this : take i l ++ drop i l = l
⊢ take i l = l

Proof state:
α : Type u_1
i : Nat
l : List α
h : l.length ≤ i
this : take i l ++ drop i l = l
⊢ take i l = l

Tactic:
rw [drop_of_length_le h, append_nil] at this

Result:
α : Type u_1
i : Nat
l : List α
h : l.length ≤ i
this : take i l = l
⊢ take i l = l
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma π_symm (i₁ : I₁) (i₂ : I₂) :
    π c₂ c₁ c₁₂ ⟨i₂, i₁⟩ = π c₁ c₂ c₁₂ ⟨i₁, i₂⟩

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)

Tactic:
apply TotalComplexShapeSymmetry.symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_univ : IntegrableOn f univ μ ↔ Integrable f μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
⊢ IntegrableOn f univ μ ↔ Integrable f μ

Tactic:
rw [IntegrableOn, Measure.restrict_univ]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
lemma ofSign_disjoint : _root_.Disjoint (ofSign 1 : Finset (Perm α)) (ofSign (-1))

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
⊢ False

Tactic:
have := hσ.symm.trans hτ

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
this : 1 = -1
⊢ False

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
this : 1 = -1
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ _root_.Disjoint (ofSign 1) (ofSign (-1))

Tactic:
rw [Finset.disjoint_iff_ne]

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ a ∈ ofSign 1, ∀ b ∈ ofSign (-1), a ≠ b

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ a ∈ ofSign 1, ∀ b ∈ ofSign (-1), a ≠ b

Tactic:
rintro σ hσ τ hτ rfl

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ ∈ ofSign 1
hτ : σ ∈ ofSign (-1)
⊢ False

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ ∈ ofSign 1
hτ : σ ∈ ofSign (-1)
⊢ False

Tactic:
rw [mem_ofSign] at hσ hτ

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w

Proof state:
case pred
w n i : Nat
h : i < w
⊢ ((0#w).sshiftRight n).getLsbD i = (0#w).getLsbD i

Tactic:
simp [getLsbD_sshiftRight, h]

Result:
no goals

Proof state:
w n : Nat
⊢ (0#w).sshiftRight n = 0#w

Tactic:
ext i h

Result:
case pred
w n i : Nat
h : i < w
⊢ ((0#w).sshiftRight n).getLsbD i = (0#w).getLsbD i
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldr_reverse {α β : Type _} {t : RBNode α} {f : α → β → β} {init : β} :
    t.reverse.foldr f init = t.foldl (flip f) init :=
  foldl_reverse.symm.trans (by simp; rfl)

Proof state:
α : Type u_1
β : Type u_2
t : RBNode α
f : α → β → β
init : β
⊢ foldl (fun a b => f b a) init t = foldl (flip f) init t

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : RBNode α
f : α → β → β
init : β
⊢ foldl (fun a b => f b a) init t.reverse.reverse = foldl (flip f) init t

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
t : RBNode α
f : α → β → β
init : β
⊢ foldl (fun a b => f b a) init t = foldl (flip f) init t
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_find (n : ℕ) (h : ∀ m ≤ n, ¬P m) : (n : PartENat) < find P

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
h₂ : P (Nat.find h₁)
⊢ n < Nat.find h₁

Tactic:
revert h₂

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ P (Nat.find h₁) → n < Nat.find h₁

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ P (Nat.find h₁) → n < Nat.find h₁

Tactic:
contrapose!

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ Nat.find h₁ ≤ n → ¬P (Nat.find h₁)

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
⊢ ↑n < find P

Tactic:
rw [coe_lt_iff]

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
⊢ ∀ (h : (find P).Dom), n < (find P).get h

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ n < Nat.find h₁

Tactic:
have h₂ := @Nat.find_spec P _ h₁

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
h₂ : P (Nat.find h₁)
⊢ n < Nat.find h₁

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ Nat.find h₁ ≤ n → ¬P (Nat.find h₁)

Tactic:
exact h _

Result:
no goals

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ n < (find P).get h₁

Tactic:
rw [find_get]

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ n < Nat.find h₁

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
⊢ ∀ (h : (find P).Dom), n < (find P).get h

Tactic:
intro h₁

Result:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ m ≤ n, ¬P m
h₁ : (find P).Dom
⊢ n < (find P).get h₁
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_pow_le_one_div_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :
    1 / a ^ n ≤ 1 / a ^ m

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn) <;>
  exact pow_pos (zero_lt_one.trans_le a1) _

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem vars_sub_subset [DecidableEq σ] : (p - q).vars ⊆ p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (p - q).vars ⊆ p.vars ∪ q.vars

Tactic:
convert vars_add_subset p (-q) using 2 <;> simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_orderTop (x : HahnSeries Γ (Rᵃᵒᵖ)) :
    (addOppositeEquiv x).unop.orderTop = x.orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv x)).orderTop = x.orderTop

Tactic:
simp only [orderTop, AddOpposite.unop_op, mk_eq_zero, EmbeddingLike.map_eq_zero_iff,
  addOppositeEquiv_support, ne_eq]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else ↑(⋯.min ⋯)) =
    if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else ↑(⋯.min ⋯)

Tactic:
simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Tactic:
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, coeff_zero]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Tactic:
simp_rw [HahnSeries.ext_iff, funext_iff]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else ↑(⋯.min ⋯)) =
    if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else ↑(⋯.min ⋯)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv x)).orderTop = x.orderTop

Tactic:
classical
simp only [orderTop, AddOpposite.unop_op, mk_eq_zero, EmbeddingLike.map_eq_zero_iff,
  addOppositeEquiv_support, ne_eq]
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, coeff_zero]
simp_rw [HahnSeries.ext_iff, funext_iff]
simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

Result:
no goals
-- Mathlib/Data/Set/MulAntidiagonal.lean
theorem fst_eq_fst_iff_snd_eq_snd : (x : α × α).1 = (y : α × α).1 ↔ (x : α × α).2 = (y : α × α).2 :=
  ⟨fun h =>
    mul_left_cancel
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm,
    fun h =>
    mul_right_cancel
      (y.2.2.2.trans <| by
          rw [← h]
          exact x.2.2.2.symm).symm⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑x).2

Tactic:
exact x.2.2.2.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑x).1 * (↑x).2

Tactic:
exact x.2.2.2.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑y).2

Tactic:
rw [← h]

Result:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑x).2

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 * (↑x).2

Tactic:
rw [← h]

Result:
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑x).1 * (↑x).2
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- Rewrite for `InterpStrip` when `0 < sSupNormIm f 0` and `0 < sSupNormIm f 1`. -/
lemma interpStrip_eq_of_pos (z : ℂ) (h0 : 0 < sSupNormIm f 0) (h1 : 0 < sSupNormIm f 1) :
    interpStrip f z = sSupNormIm f 0 ^ (1 - z) * sSupNormIm f 1 ^ z

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
h0 : 0 < sSupNormIm f 0
h1 : 0 < sSupNormIm f 1
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
simp only [ne_of_gt h0, ne_of_gt h1, interpStrip, if_false, or_false]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_commonNeighbors_top [DecidableEq V] {v w : V} (h : v ≠ w) :
    Fintype.card ((⊤ : SimpleGraph V).commonNeighbors v w) = Fintype.card V - 2

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ #Set.univ.toFinset - #{v, w}.toFinset = Fintype.card V - 2

Tactic:
simp [Finset.card_univ, h]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ {v, w}.toFinset ⊆ Set.univ.toFinset

Tactic:
simp only [Set.toFinset_subset_toFinset, Set.subset_univ]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2

Tactic:
simp only [commonNeighbors_top_eq, ← Set.toFinset_card, Set.toFinset_diff]

Result:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ #(Set.univ.toFinset \ {v, w}.toFinset) = Fintype.card V - 2

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ #(Set.univ.toFinset \ {v, w}.toFinset) = Fintype.card V - 2

Tactic:
rw [Finset.card_sdiff]

Result:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ #Set.univ.toFinset - #{v, w}.toFinset = Fintype.card V - 2

V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ {v, w}.toFinset ⊆ Set.univ.toFinset
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_swap' (a : Array α) (i j : Nat) {hi hj} (k : Nat) (hk : k < a.size) :
    (a.swap i j hi hj)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k]

Proof state:
case isFalse
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
h✝ : ¬k = i
⊢ (a.swap i j hi hj)[k] = if k = j then a[i] else a[k]

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
⊢ (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Tactic:
split

Result:
case isTrue
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
h✝ : k = i
⊢ (a.swap i j hi hj)[k] = a[j]

case isFalse
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
h✝ : ¬k = i
⊢ (a.swap i j hi hj)[k] = if k = j then a[i] else a[k]

Proof state:
α : Type ?u.520875
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
⊢ k < (a.swap i j hi hj).size

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
hk : k < a.size
h✝ : k = i
⊢ (a.swap i j hi hj)[k] = a[j]

Tactic:
simp_all only [getElem_swap_left]

Result:
no goals
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmoothOfRelativeDimension_isStableUnderBaseChange :
    IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension.{t, w} n)

Proof state:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r✝ : R
x✝ : T
⊢ (algebraMap R T) r✝ * x✝ = (algebraMap R T) r✝ * x✝

Proof state:
case h.e'_6
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.TensorProduct.includeLeftRingHom.toAlgebra = Algebra.TensorProduct.leftAlgebra

Tactic:
ext

Result:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := Algebra.TensorProduct.includeLeftRingHom.toAlgebra;
    r✝ • x✝) =
    r✝ • x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.convertLRAT_readyForRatAdd (cnf : CNF Nat) :
    DefaultFormula.ReadyForRatAdd (CNF.convertLRAT cnf)

Proof state:
cnf : CNF Nat
⊢ (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray).ReadyForRatAdd

Tactic:
apply DefaultFormula.readyForRatAdd_ofArray

Result:
no goals

Proof state:
cnf : CNF Nat
⊢ (convertLRAT cnf).ReadyForRatAdd

Tactic:
unfold CNF.convertLRAT

Result:
cnf : CNF Nat
⊢ (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray).ReadyForRatAdd
-- Mathlib/Topology/ContinuousOn.lean
theorem Continuous.continuousOn (h : Continuous f) : ContinuousOn f s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s

Tactic:
exact h.mono (subset_univ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : Continuous f
⊢ ContinuousOn f s

Tactic:
rw [continuous_iff_continuousOn_univ] at h

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mul_mem_cancel_left {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈ S.arrows c d) :
    f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e

Tactic:
apply S.mul (S.inv hf) h

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
this : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e

Tactic:
simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e

Tactic:
apply S.mul hf

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e

Tactic:
rintro h

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ g ∈ S.arrows d e

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ g ∈ S.arrows d e

Tactic:
suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
  simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e
-- Mathlib/Analysis/Complex/Convex.lean
lemma Complex.isConnected_of_lowerHalfPlane {r} {s : Set ℂ} (hs₁ : {z | z.im < r} ⊆ s)
    (hs₂ : s ⊆ {z | z.im ≤ r}) : IsConnected s

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ (↑r - 1) * I ∈ {c | c.im < r}

Tactic:
simp

Result:
no goals

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ s ⊆ closure {z | z.im < r}

Tactic:
simpa only [closure_setOf_im_lt] using hs₂

Result:
no goals

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ IsConnected s

Tactic:
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_im_lt] using hs₂)

Result:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ IsConnected {z | z.im < r}

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ IsConnected {z | z.im < r}

Tactic:
exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
theorem Group.ext {G : Type*} ⦃g₁ g₂ : Group G⦄ (h_mul : g₁.mul = g₂.mul) : g₁ = g₂

Proof state:
G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ g₁ = g₂

Tactic:
exact
  Group.toDivInvMonoid_injective
    (DivInvMonoid.ext h_mul
      (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))

Result:
no goals

Proof state:
G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
⊢ g₁ = g₂

Tactic:
let f : @MonoidHom G G g₁.toMulOneClass g₂.toMulOneClass :=
  @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
    (fun x y => congr_fun (congr_fun h_mul x) y)

Result:
G : Type u_1
g₁ g₂ : Group G
h_mul : Mul.mul = Mul.mul
h₁ : One.one = One.one
f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ g₁ = g₂
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousAt_iff_right {p : κ → Prop} {s : κ → Set (α × α)}
    {F : ι → X → α} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
    EquicontinuousAt F x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k